Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem caucvglem2 7094

Description: Lemma for caucvg 7099. is a nonempty bounded subset of .

Hypotheses

Ref	Expression
caucvg.1
caucvg.2
caucvg.3

Assertion

Ref	Expression
caucvglem2

Distinct variable groups:   ,,,,,,,   ,,,,

---

Proof of Theorem caucvglem2

Step	Hyp	Ref	Expression
1		caucvg.3	. . 3
2		ssrab2 2121	. . 3
3	1, 2	eqsstr 2081	. 2
4		caucvg.1	. . . . 5
5		axresscn 5240	. . . . 5
6		fss 3620	. . . . 5
7	4, 5, 6	mp2an 695	. . . 4
8		caucvg.2	. . . 4
9	7, 8	caubnd 6863	. . 3
10		absltt 6817	. . . . . . . . . . . . . 14
11		pm3.26 319	. . . . . . . . . . . . . 14
12	10, 11	syl6bi 214	. . . . . . . . . . . . 13
13	4	ffvelrni 3800	. . . . . . . . . . . . 13
14	12, 13	sylan 448	. . . . . . . . . . . 12
15	14	ancoms 436	. . . . . . . . . . 11
16	15	a1dd 42	. . . . . . . . . 10
17	16	r19.20dva 1701	. . . . . . . . 9
18		1nn 5882	. . . . . . . . . 10
19	18	a1i 8	. . . . . . . . 9
20	17, 19	jctild 599	. . . . . . . 8
21		breq1 2612	. . . . . . . . . . 11
22	21	imbi1d 611	. . . . . . . . . 10
23	22	ralbidv 1655	. . . . . . . . 9
24	23	rcla4ev 1868	. . . . . . . 8
25	20, 24	syl6 22	. . . . . . 7
26		renegclt 5409	. . . . . . 7
27	25, 26	jctild 599	. . . . . 6
28	4, 8, 1	caucvglem1 7093	. . . . . 6
29	27, 28	syl6ibr 213	. . . . 5
30		ne0i 2276	. . . . 5
31	29, 30	syl6 22	. . . 4
32	31	r19.23aiv 1735	. . 3
33	9, 32	ax-mp 7	. 2
34	4, 8, 1	caucvglem1 7093	. . . . . . 7
35		nnret 5877	. . . . . . . . . . . . . . . . . 18
36		leidt 5504	. . . . . . . . . . . . . . . . . 18
37	35, 36	syl 10	. . . . . . . . . . . . . . . . 17
38		breq2 2613	. . . . . . . . . . . . . . . . . . 19
39		fveq2 3709	. . . . . . . . . . . . . . . . . . . 20
40	39	breq2d 2620	. . . . . . . . . . . . . . . . . . 19
41	38, 40	imbi12d 624	. . . . . . . . . . . . . . . . . 18
42	41	rcla4v 1864	. . . . . . . . . . . . . . . . 17
43	37, 42	mpid 47	. . . . . . . . . . . . . . . 16
44	43	adantr 389	. . . . . . . . . . . . . . 15
45	39	fveq2d 3713	. . . . . . . . . . . . . . . . . . 19
46	45	breq1d 2619	. . . . . . . . . . . . . . . . . 18
47	46	rcla4v 1864	. . . . . . . . . . . . . . . . 17
48	47	adantr 389	. . . . . . . . . . . . . . . 16
49		absltt 6817	. . . . . . . . . . . . . . . . . 18
50	4	ffvelrni 3800	. . . . . . . . . . . . . . . . . 18
51	49, 50	sylan 448	. . . . . . . . . . . . . . . . 17
52		pm3.27 323	. . . . . . . . . . . . . . . . 17
53	51, 52	syl6bi 214	. . . . . . . . . . . . . . . 16
54	48, 53	syld 27	. . . . . . . . . . . . . . 15
55	44, 54	anim12d 556	. . . . . . . . . . . . . 14
56	55	3adant1 795	. . . . . . . . . . . . 13
57		axlttrn 5476	. . . . . . . . . . . . . . 15
58	57, 50	syl3an2 858	. . . . . . . . . . . . . 14
59		ltlet 5493	. . . . . . . . . . . . . . 15
60	59	3adant2 796	. . . . . . . . . . . . . 14
61	58, 60	syld 27	. . . . . . . . . . . . 13
62	56, 61	syld 27	. . . . . . . . . . . 12