Theorem altretop 14997

Description: Alternate definition of the standard topology of the reals. (Morris. Def. 2.1.1 p. 34). Morris calls the standard topology of the reals the euclidean topology.

Assertion

Ref	Expression
altretop	|- (A e. (topGen` ran (,)) <-> (A C_ RR /\ A.y e. A E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))

Distinct variable group:   A,a,b,y

Proof of Theorem altretop

Step	Hyp	Ref	Expression
1		altretoplem2 14996	. 2 |- (A e. (topGen` ran (,)) <-> (A C_ RR /\ A.y e. A E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A)))
2		elxr 6706	. . . . . . . 8 |- (u e. RR* <-> (u e. RR \/ u = +oo \/ u = -oo))
3		elxr 6706	. . . . . . . . . 10 |- (v e. RR* <-> (v e. RR \/ v = +oo \/ v = -oo))
4		anddi2 14268	. . . . . . . . . . . 12 |- (((v e. RR \/ v = +oo \/ v = -oo) /\ (u e. RR \/ u = +oo \/ u = -oo)) <-> (((v e. RR /\ u e. RR) \/ (v e. RR /\ u = +oo) \/ (v e. RR /\ u = -oo)) \/ ((v = +oo /\ u e. RR) \/ (v = +oo /\ u = +oo) \/ (v = +oo /\ u = -oo)) \/ ((v = -oo /\ u e. RR) \/ (v = -oo /\ u = +oo) \/ (v = -oo /\ u = -oo))))
5		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- (a = u -> (a(,)b) = (u(,)b))
6	5	eleq2d 1964	. . . . . . . . . . . . . . . . . 18 |- (a = u -> (y e. (a(,)b) <-> y e. (u(,)b)))
7	5	sseq1d 2644	. . . . . . . . . . . . . . . . . 18 |- (a = u -> ((a(,)b) C_ A <-> (u(,)b) C_ A))
8	6, 7	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (a = u -> ((y e. (a(,)b) /\ (a(,)b) C_ A) <-> (y e. (u(,)b) /\ (u(,)b) C_ A)))
9		opreq2 4890	. . . . . . . . . . . . . . . . . . 19 |- (b = v -> (u(,)b) = (u(,)v))
10	9	eleq2d 1964	. . . . . . . . . . . . . . . . . 18 |- (b = v -> (y e. (u(,)b) <-> y e. (u(,)v)))
11	9	sseq1d 2644	. . . . . . . . . . . . . . . . . 18 |- (b = v -> ((u(,)b) C_ A <-> (u(,)v) C_ A))
12	10, 11	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (b = v -> ((y e. (u(,)b) /\ (u(,)b) C_ A) <-> (y e. (u(,)v) /\ (u(,)v) C_ A)))
13	8, 12	rcla42ev 2385	. . . . . . . . . . . . . . . 16 |- ((u e. RR /\ v e. RR /\ (y e. (u(,)v) /\ (u(,)v) C_ A)) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
14	13	3expia 1069	. . . . . . . . . . . . . . 15 |- ((u e. RR /\ v e. RR) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
15	14	ancoms 484	. . . . . . . . . . . . . 14 |- ((v e. RR /\ u e. RR) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
16		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (u = +oo -> (u(,)v) = ( +oo(,)v))
17	16	eleq2d 1964	. . . . . . . . . . . . . . . . . . 19 |- (u = +oo -> (y e. (u(,)v) <-> y e. ( +oo(,)v)))
18	17	biimpd 170	. . . . . . . . . . . . . . . . . 18 |- (u = +oo -> (y e. (u(,)v) -> y e. ( +oo(,)v)))
19		oisbmj 14848	. . . . . . . . . . . . . . . . . . . 20 |- ( +oo(,)v) = (/)
20	19	eleq2i 1961	. . . . . . . . . . . . . . . . . . 19 |- (y e. ( +oo(,)v) <-> y e. (/))
21		noel 2879	. . . . . . . . . . . . . . . . . . . 20 |- -. y e. (/)
22	21	pm2.21i 93	. . . . . . . . . . . . . . . . . . 19 |- (y e. (/) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
23	20, 22	sylbi 216	. . . . . . . . . . . . . . . . . 18 |- (y e. ( +oo(,)v) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
24	18, 23	syl6com 64	. . . . . . . . . . . . . . . . 17 |- (y e. (u(,)v) -> (u = +oo -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
25	24	adantr 425	. . . . . . . . . . . . . . . 16 |- ((y e. (u(,)v) /\ (u(,)v) C_ A) -> (u = +oo -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
26	25	com12 14	. . . . . . . . . . . . . . 15 |- (u = +oo -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
27	26	adantl 424	. . . . . . . . . . . . . 14 |- ((v e. RR /\ u = +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
28		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (u = -oo -> (u(,)v) = ( -oo(,)v))
29	28	eleq2d 1964	. . . . . . . . . . . . . . . . 17 |- (u = -oo -> (y e. (u(,)v) <-> y e. ( -oo(,)v)))
30	28	sseq1d 2644	. . . . . . . . . . . . . . . . 17 |- (u = -oo -> ((u(,)v) C_ A <-> ( -oo(,)v) C_ A))
31	29, 30	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (u = -oo -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A)))
32	31	adantl 424	. . . . . . . . . . . . . . 15 |- ((v e. RR /\ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A)))
33		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (b = v -> (a(,)b) = (a(,)v))
34	33	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = v -> (y e. (a(,)b) <-> y e. (a(,)v)))
35	33	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = v -> ((a(,)b) C_ A <-> (a(,)v) C_ A))
36	34, 35	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- (b = v -> ((y e. (a(,)b) /\ (a(,)b) C_ A) <-> (y e. (a(,)v) /\ (a(,)v) C_ A)))
37	36	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . 21 |- (b = v -> (E.a e. RR (y e. (a(,)b) /\ (a(,)b) C_ A) <-> E.a e. RR (y e. (a(,)v) /\ (a(,)v) C_ A)))
38	37	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- ((v e. RR /\ E.a e. RR (y e. (a(,)v) /\ (a(,)v) C_ A)) -> E.b e. RR E.a e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
39	38	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (v e. RR -> (E.a e. RR (y e. (a(,)v) /\ (a(,)v) C_ A) -> E.b e. RR E.a e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
40		elioore 7554	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. ( -oo(,)v) -> y e. RR)
41		1re 6598	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. RR
42	40, 41	jctir 317	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. ( -oo(,)v) -> (y e. RR /\ 1 e. RR))
43		resubcl 6601	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. RR /\ 1 e. RR) -> (y - 1) e. RR)
44	42, 43	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. ( -oo(,)v) -> (y - 1) e. RR)
45	44	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> (y - 1) e. RR)
46		visset 2295	. . . . . . . . . . . . . . . . . . . . . . 23 |- v e. _V
47		elioo4g 7553	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. _V -> (y e. ( -oo(,)v) <-> (( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v))))
48	46, 47	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. ( -oo(,)v) <-> (( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)))
49		peano2rem 6605	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. RR -> (y - 1) e. RR)
50		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y - 1) e. RR -> (y - 1) e. RR*)
51	49, 50	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. RR -> (y - 1) e. RR*)
52	51	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (( -oo e. RR* /\ v e. RR* /\ y e. RR) -> (y - 1) e. RR*)
53	52	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> (y - 1) e. RR*)
54		simpl2 880	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> v e. RR*)
55		simpl3 881	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> y e. RR)
56	53, 54, 55	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> ((y - 1) e. RR* /\ v e. RR* /\ y e. RR))
57		ltm1 6993	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. RR -> (y - 1) < y)
58	57	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (( -oo e. RR* /\ v e. RR* /\ y e. RR) -> (y - 1) < y)
59	58	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> (y - 1) < y)
60		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> y < v)
61	59, 60	jca 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> ((y - 1) < y /\ y < v))
62	56, 61	jca 310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> (((y - 1) e. RR* /\ v e. RR* /\ y e. RR) /\ ((y - 1) < y /\ y < v)))
63	46	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> v e. _V)
64		elioo4g 7553	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. _V -> (y e. ((y - 1)(,)v) <-> (((y - 1) e. RR* /\ v e. RR* /\ y e. RR) /\ ((y - 1) < y /\ y < v))))
65	63, 64	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> (y e. ((y - 1)(,)v) <-> (((y - 1) e. RR* /\ v e. RR* /\ y e. RR) /\ ((y - 1) < y /\ y < v))))
66	62, 65	mpbird 213	. . . . . . . . . . . . . . . . . . . . . 22 |- ((( -oo e. RR* /\ v e. RR* /\ y e. RR) /\ ( -oo < y /\ y < v)) -> y e. ((y - 1)(,)v))
67	48, 66	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. ( -oo(,)v) -> y e. ((y - 1)(,)v))
68		oibbi2 14854	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y - 1)(,)v) C_ ( -oo(,)v)
69		sstr 2625	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((y - 1)(,)v) C_ ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> ((y - 1)(,)v) C_ A)
70	68, 69	mpan 759	. . . . . . . . . . . . . . . . . . . . 21 |- (( -oo(,)v) C_ A -> ((y - 1)(,)v) C_ A)
71	67, 70	anim12i 360	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> (y e. ((y - 1)(,)v) /\ ((y - 1)(,)v) C_ A))
72		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = (y - 1) -> (a(,)v) = ((y - 1)(,)v))
73	72	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (y - 1) -> (y e. (a(,)v) <-> y e. ((y - 1)(,)v)))
74	72	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (y - 1) -> ((a(,)v) C_ A <-> ((y - 1)(,)v) C_ A))
75	73, 74	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (a = (y - 1) -> ((y e. (a(,)v) /\ (a(,)v) C_ A) <-> (y e. ((y - 1)(,)v) /\ ((y - 1)(,)v) C_ A)))
76	75	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- (((y - 1) e. RR /\ (y e. ((y - 1)(,)v) /\ ((y - 1)(,)v) C_ A)) -> E.a e. RR (y e. (a(,)v) /\ (a(,)v) C_ A))
77	45, 71, 76	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> E.a e. RR (y e. (a(,)v) /\ (a(,)v) C_ A))
78	39, 77	syl5com 63	. . . . . . . . . . . . . . . . . 18 |- ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> (v e. RR -> E.b e. RR E.a e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
79		rexcom 2243	. . . . . . . . . . . . . . . . . 18 |- (E.b e. RR E.a e. RR (y e. (a(,)b) /\ (a(,)b) C_ A) <-> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
80	78, 79	syl6ib 229	. . . . . . . . . . . . . . . . 17 |- ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> (v e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
81	80	com12 14	. . . . . . . . . . . . . . . 16 |- (v e. RR -> ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
82	81	adantr 425	. . . . . . . . . . . . . . 15 |- ((v e. RR /\ u = -oo) -> ((y e. ( -oo(,)v) /\ ( -oo(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
83	32, 82	sylbid 220	. . . . . . . . . . . . . 14 |- ((v e. RR /\ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
84	15, 27, 83	3jaoi 1160	. . . . . . . . . . . . 13 |- (((v e. RR /\ u e. RR) \/ (v e. RR /\ u = +oo) \/ (v e. RR /\ u = -oo)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
85		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (v = +oo -> (u(,)v) = (u(,) +oo))
86	85	eleq2d 1964	. . . . . . . . . . . . . . . . 17 |- (v = +oo -> (y e. (u(,)v) <-> y e. (u(,) +oo)))
87	85	sseq1d 2644	. . . . . . . . . . . . . . . . 17 |- (v = +oo -> ((u(,)v) C_ A <-> (u(,) +oo) C_ A))
88	86, 87	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (v = +oo -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. (u(,) +oo) /\ (u(,) +oo) C_ A)))
89	88	adantr 425	. . . . . . . . . . . . . . 15 |- ((v = +oo /\ u e. RR) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. (u(,) +oo) /\ (u(,) +oo) C_ A)))
90		elioore 7554	. . . . . . . . . . . . . . . . . . 19 |- (y e. (u(,) +oo) -> y e. RR)
91		peano2re 6599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. RR -> (y + 1) e. RR)
92		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (b = (y + 1) -> (u(,)b) = (u(,)(y + 1)))
93	92	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (b = (y + 1) -> (y e. (u(,)b) <-> y e. (u(,)(y + 1))))
94	92	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (b = (y + 1) -> ((u(,)b) C_ A <-> (u(,)(y + 1)) C_ A))
95	93, 94	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (b = (y + 1) -> ((y e. (u(,)b) /\ (u(,)b) C_ A) <-> (y e. (u(,)(y + 1)) /\ (u(,)(y + 1)) C_ A)))
96	95	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((y + 1) e. RR /\ (y e. (u(,)(y + 1)) /\ (u(,)(y + 1)) C_ A)) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A))
97	96	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y + 1) e. RR -> ((y e. (u(,)(y + 1)) /\ (u(,)(y + 1)) C_ A) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A)))
98		elioooord 14855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (y e. (u(,) +oo) -> (u < y /\ y < +oo))
99	98	simplld 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. (u(,) +oo) -> u < y)
100	99	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> u < y)
101		ltp1 6989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (y e. RR -> y < (y + 1))
102	90, 101	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. (u(,) +oo) -> y < (y + 1))
103	102	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> y < (y + 1))
104	100, 103	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (u < y /\ y < (y + 1)))
105		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. RR -> u e. RR*)
106	105	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((u e. RR /\ (u(,) +oo) C_ A) -> u e. RR*)
107	106	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> u e. RR*)
108		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((y + 1) e. RR -> (y + 1) e. RR*)
109	108	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (y + 1) e. RR*)
110		rexr 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (y e. RR -> y e. RR*)
111	90, 110	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. (u(,) +oo) -> y e. RR*)
112	111	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> y e. RR*)
113		elioo5 7552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u e. RR* /\ (y + 1) e. RR* /\ y e. RR*) -> (y e. (u(,)(y + 1)) <-> (u < y /\ y < (y + 1))))
114	107, 109, 112, 113	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (y e. (u(,)(y + 1)) <-> (u < y /\ y < (y + 1))))
115	104, 114	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> y e. (u(,)(y + 1)))
116		pnfxr 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- +oo e. RR*
117	116	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> +oo e. RR*)
118		pnfge 6723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((y + 1) e. RR* -> (y + 1) <_ +oo)
119	108, 118	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((y + 1) e. RR -> (y + 1) <_ +oo)
120	119	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (y + 1) <_ +oo)
121		iooss2 7541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((u e. RR* /\ (y + 1) e. RR* /\ +oo e. RR*) /\ (y + 1) <_ +oo) -> (u(,)(y + 1)) C_ (u(,) +oo))
122	107, 109, 117, 120, 121	syl31anc 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (u(,)(y + 1)) C_ (u(,) +oo))
123		simp2r 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (u(,) +oo) C_ A)
124	122, 123	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (u(,)(y + 1)) C_ A)
125	115, 124	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> (y e. (u(,)(y + 1)) /\ (u(,)(y + 1)) C_ A))
126	97, 125	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y + 1) e. RR -> (((y + 1) e. RR /\ (u e. RR /\ (u(,) +oo) C_ A) /\ y e. (u(,) +oo)) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A)))
127	126	3expd 1085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y + 1) e. RR -> ((y + 1) e. RR -> ((u e. RR /\ (u(,) +oo) C_ A) -> (y e. (u(,) +oo) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A)))))
128	91, 91, 127	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. RR -> ((u e. RR /\ (u(,) +oo) C_ A) -> (y e. (u(,) +oo) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A))))
129	128	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u e. RR /\ (u(,) +oo) C_ A) -> (y e. RR -> (y e. (u(,) +oo) -> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A))))
130	8	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a = u -> (E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A) <-> E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A)))
131	130	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((u e. RR /\ E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A)) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
132	131	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.b e. RR (y e. (u(,)b) /\ (u(,)b) C_ A) -> (u e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
133	129, 132	syl8 27	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u e. RR /\ (u(,) +oo) C_ A) -> (y e. RR -> (y e. (u(,) +oo) -> (u e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))))
134	133	com34 40	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((u e. RR /\ (u(,) +oo) C_ A) -> (y e. RR -> (u e. RR -> (y e. (u(,) +oo) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))))
135	134	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. RR -> ((u(,) +oo) C_ A -> (y e. RR -> (u e. RR -> (y e. (u(,) +oo) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))))
136	135	com24 41	. . . . . . . . . . . . . . . . . . . . 21 |- (u e. RR -> (u e. RR -> (y e. RR -> ((u(,) +oo) C_ A -> (y e. (u(,) +oo) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))))
137	136	pm2.43i 78	. . . . . . . . . . . . . . . . . . . 20 |- (u e. RR -> (y e. RR -> ((u(,) +oo) C_ A -> (y e. (u(,) +oo) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))))
138	137	com14 42	. . . . . . . . . . . . . . . . . . 19 |- (y e. (u(,) +oo) -> (y e. RR -> ((u(,) +oo) C_ A -> (u e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))))
139	90, 138	mpd 29	. . . . . . . . . . . . . . . . . 18 |- (y e. (u(,) +oo) -> ((u(,) +oo) C_ A -> (u e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))
140	139	imp 377	. . . . . . . . . . . . . . . . 17 |- ((y e. (u(,) +oo) /\ (u(,) +oo) C_ A) -> (u e. RR -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
141	140	com12 14	. . . . . . . . . . . . . . . 16 |- (u e. RR -> ((y e. (u(,) +oo) /\ (u(,) +oo) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
142	141	adantl 424	. . . . . . . . . . . . . . 15 |- ((v = +oo /\ u e. RR) -> ((y e. (u(,) +oo) /\ (u(,) +oo) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
143	89, 142	sylbid 220	. . . . . . . . . . . . . 14 |- ((v = +oo /\ u e. RR) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
144	16	adantl 424	. . . . . . . . . . . . . . 15 |- ((v = +oo /\ u = +oo) -> (u(,)v) = ( +oo(,)v))
145		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- ((u(,)v) = (/) -> (y e. (u(,)v) <-> y e. (/)))
146	145	biimpd 170	. . . . . . . . . . . . . . . . . . 19 |- ((u(,)v) = (/) -> (y e. (u(,)v) -> y e. (/)))
147	146, 22	syl6com 64	. . . . . . . . . . . . . . . . . 18 |- (y e. (u(,)v) -> ((u(,)v) = (/) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
148	147	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((y e. (u(,)v) /\ (u(,)v) C_ A) -> ((u(,)v) = (/) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
149		eqtr 1904	. . . . . . . . . . . . . . . . 17 |- (((u(,)v) = ( +oo(,)v) /\ ( +oo(,)v) = (/)) -> (u(,)v) = (/))
150	148, 149	syl5com 63	. . . . . . . . . . . . . . . 16 |- (((u(,)v) = ( +oo(,)v) /\ ( +oo(,)v) = (/)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
151	19, 150	mpan2 760	. . . . . . . . . . . . . . 15 |- ((u(,)v) = ( +oo(,)v) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
152	144, 151	syl 12	. . . . . . . . . . . . . 14 |- ((v = +oo /\ u = +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
153		opreq12 4891	. . . . . . . . . . . . . . . 16 |- ((u = -oo /\ v = +oo) -> (u(,)v) = ( -oo(,) +oo))
154		ioomax 7561	. . . . . . . . . . . . . . . . . . 19 |- ( -oo(,) +oo) = RR
155	154	eqeq2i 1894	. . . . . . . . . . . . . . . . . 18 |- ((u(,)v) = ( -oo(,) +oo) <-> (u(,)v) = RR)
156		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- ((u(,)v) = RR -> (y e. (u(,)v) <-> y e. RR))
157		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- ((u(,)v) = RR -> ((u(,)v) C_ A <-> RR C_ A))
158	156, 157	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- ((u(,)v) = RR -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. RR /\ RR C_ A)))
159	158	biimpd 170	. . . . . . . . . . . . . . . . . 18 |- ((u(,)v) = RR -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> (y e. RR /\ RR C_ A)))
160	155, 159	sylbi 216	. . . . . . . . . . . . . . . . 17 |- ((u(,)v) = ( -oo(,) +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> (y e. RR /\ RR C_ A)))
161	49	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((y e. RR /\ RR C_ A) -> (y - 1) e. RR)
162	91	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((y e. RR /\ RR C_ A) -> (y + 1) e. RR)
163		1rp 7235	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR+
164		cbci 14852	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ 1 e. RR+) -> y e. ((y - 1)(,)(y + 1)))
165	163, 164	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR -> y e. ((y - 1)(,)(y + 1)))
166		ioossre 7557	. . . . . . . . . . . . . . . . . . . 20 |- ((y - 1)(,)(y + 1)) C_ RR
167		sstr 2625	. . . . . . . . . . . . . . . . . . . 20 |- ((((y - 1)(,)(y + 1)) C_ RR /\ RR C_ A) -> ((y - 1)(,)(y + 1)) C_ A)
168	166, 167	mpan 759	. . . . . . . . . . . . . . . . . . 19 |- (RR C_ A -> ((y - 1)(,)(y + 1)) C_ A)
169	165, 168	anim12i 360	. . . . . . . . . . . . . . . . . 18 |- ((y e. RR /\ RR C_ A) -> (y e. ((y - 1)(,)(y + 1)) /\ ((y - 1)(,)(y + 1)) C_ A))
170		opreq1 4889	. . . . . . . . . . . . . . . . . . . . 21 |- (a = (y - 1) -> (a(,)b) = ((y - 1)(,)b))
171	170	eleq2d 1964	. . . . . . . . . . . . . . . . . . . 20 |- (a = (y - 1) -> (y e. (a(,)b) <-> y e. ((y - 1)(,)b)))
172	170	sseq1d 2644	. . . . . . . . . . . . . . . . . . . 20 |- (a = (y - 1) -> ((a(,)b) C_ A <-> ((y - 1)(,)b) C_ A))
173	171, 172	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (a = (y - 1) -> ((y e. (a(,)b) /\ (a(,)b) C_ A) <-> (y e. ((y - 1)(,)b) /\ ((y - 1)(,)b) C_ A)))
174		opreq2 4890	. . . . . . . . . . . . . . . . . . . . 21 |- (b = (y + 1) -> ((y - 1)(,)b) = ((y - 1)(,)(y + 1)))
175	174	eleq2d 1964	. . . . . . . . . . . . . . . . . . . 20 |- (b = (y + 1) -> (y e. ((y - 1)(,)b) <-> y e. ((y - 1)(,)(y + 1))))
176	174	sseq1d 2644	. . . . . . . . . . . . . . . . . . . 20 |- (b = (y + 1) -> (((y - 1)(,)b) C_ A <-> ((y - 1)(,)(y + 1)) C_ A))
177	175, 176	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (b = (y + 1) -> ((y e. ((y - 1)(,)b) /\ ((y - 1)(,)b) C_ A) <-> (y e. ((y - 1)(,)(y + 1)) /\ ((y - 1)(,)(y + 1)) C_ A)))
178	173, 177	rcla42ev 2385	. . . . . . . . . . . . . . . . . 18 |- (((y - 1) e. RR /\ (y + 1) e. RR /\ (y e. ((y - 1)(,)(y + 1)) /\ ((y - 1)(,)(y + 1)) C_ A)) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
179	161, 162, 169, 178	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((y e. RR /\ RR C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
180	160, 179	syl6 25	. . . . . . . . . . . . . . . 16 |- ((u(,)v) = ( -oo(,) +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
181	153, 180	syl 12	. . . . . . . . . . . . . . 15 |- ((u = -oo /\ v = +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
182	181	ancoms 484	. . . . . . . . . . . . . 14 |- ((v = +oo /\ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
183	143, 152, 182	3jaoi 1160	. . . . . . . . . . . . 13 |- (((v = +oo /\ u e. RR) \/ (v = +oo /\ u = +oo) \/ (v = +oo /\ u = -oo)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
184		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (v = -oo -> (u(,)v) = (u(,) -oo))
185		oisbmi 14847	. . . . . . . . . . . . . . . . 17 |- (u(,) -oo) = (/)
186		eqtr 1904	. . . . . . . . . . . . . . . . . 18 |- (((u(,)v) = (u(,) -oo) /\ (u(,) -oo) = (/)) -> (u(,)v) = (/))
187	148, 186	syl5com 63	. . . . . . . . . . . . . . . . 17 |- (((u(,)v) = (u(,) -oo) /\ (u(,) -oo) = (/)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
188	185, 187	mpan2 760	. . . . . . . . . . . . . . . 16 |- ((u(,)v) = (u(,) -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
189	184, 188	syl 12	. . . . . . . . . . . . . . 15 |- (v = -oo -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
190	189	adantr 425	. . . . . . . . . . . . . 14 |- ((v = -oo /\ u e. RR) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
191	189	adantr 425	. . . . . . . . . . . . . 14 |- ((v = -oo /\ u = +oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
192	189	adantr 425	. . . . . . . . . . . . . 14 |- ((v = -oo /\ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
193	190, 191, 192	3jaoi 1160	. . . . . . . . . . . . 13 |- (((v = -oo /\ u e. RR) \/ (v = -oo /\ u = +oo) \/ (v = -oo /\ u = -oo)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
194	84, 183, 193	3jaoi 1160	. . . . . . . . . . . 12 |- ((((v e. RR /\ u e. RR) \/ (v e. RR /\ u = +oo) \/ (v e. RR /\ u = -oo)) \/ ((v = +oo /\ u e. RR) \/ (v = +oo /\ u = +oo) \/ (v = +oo /\ u = -oo)) \/ ((v = -oo /\ u e. RR) \/ (v = -oo /\ u = +oo) \/ (v = -oo /\ u = -oo))) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
195	4, 194	sylbi 216	. . . . . . . . . . 11 |- (((v e. RR \/ v = +oo \/ v = -oo) /\ (u e. RR \/ u = +oo \/ u = -oo)) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
196	195	ex 402	. . . . . . . . . 10 |- ((v e. RR \/ v = +oo \/ v = -oo) -> ((u e. RR \/ u = +oo \/ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))
197	3, 196	sylbi 216	. . . . . . . . 9 |- (v e. RR* -> ((u e. RR \/ u = +oo \/ u = -oo) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))
198	197	com12 14	. . . . . . . 8 |- ((u e. RR \/ u = +oo \/ u = -oo) -> (v e. RR* -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))
199	2, 198	sylbi 216	. . . . . . 7 |- (u e. RR* -> (v e. RR* -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))))
200	199	imp 377	. . . . . 6 |- ((u e. RR* /\ v e. RR*) -> ((y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
201	200	r19.23aivv 2217	. . . . 5 |- (E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A) -> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
202		opreq1 4889	. . . . . . . . . . 11 |- (u = a -> (u(,)v) = (a(,)v))
203	202	eleq2d 1964	. . . . . . . . . 10 |- (u = a -> (y e. (u(,)v) <-> y e. (a(,)v)))
204	202	sseq1d 2644	. . . . . . . . . 10 |- (u = a -> ((u(,)v) C_ A <-> (a(,)v) C_ A))
205	203, 204	anbi12d 690	. . . . . . . . 9 |- (u = a -> ((y e. (u(,)v) /\ (u(,)v) C_ A) <-> (y e. (a(,)v) /\ (a(,)v) C_ A)))
206		opreq2 4890	. . . . . . . . . . 11 |- (v = b -> (a(,)v) = (a(,)b))
207	206	eleq2d 1964	. . . . . . . . . 10 |- (v = b -> (y e. (a(,)v) <-> y e. (a(,)b)))
208	206	sseq1d 2644	. . . . . . . . . 10 |- (v = b -> ((a(,)v) C_ A <-> (a(,)b) C_ A))
209	207, 208	anbi12d 690	. . . . . . . . 9 |- (v = b -> ((y e. (a(,)v) /\ (a(,)v) C_ A) <-> (y e. (a(,)b) /\ (a(,)b) C_ A)))
210	205, 209	rcla42ev 2385	. . . . . . . 8 |- ((a e. RR* /\ b e. RR* /\ (y e. (a(,)b) /\ (a(,)b) C_ A)) -> E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A))
211	210	3expia 1069	. . . . . . 7 |- ((a e. RR* /\ b e. RR*) -> ((y e. (a(,)b) /\ (a(,)b) C_ A) -> E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A)))
212		rexr 6668	. . . . . . 7 |- (a e. RR -> a e. RR*)
213		rexr 6668	. . . . . . 7 |- (b e. RR -> b e. RR*)
214	211, 212, 213	syl2an 503	. . . . . 6 |- ((a e. RR /\ b e. RR) -> ((y e. (a(,)b) /\ (a(,)b) C_ A) -> E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A)))
215	214	r19.23aivv 2217	. . . . 5 |- (E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A) -> E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A))
216	201, 215	impbii 174	. . . 4 |- (E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A) <-> E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
217	216	ralbii 2127	. . 3 |- (A.y e. A E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A) <-> A.y e. A E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A))
218	217	anbi2i 538	. 2 |- ((A C_ RR /\ A.y e. A E.u e. RR* E.v e. RR* (y e. (u(,)v) /\ (u(,)v) C_ A)) <-> (A C_ RR /\ A.y e. A E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))
219	1, 218	bitri 190	1 |- (A e. (topGen` ran (,)) <-> (A C_ RR /\ A.y e. A E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) C_ A)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338  ran crn 3987  ` cfv 3998  (class class class)co 4884  RRcr 6385  1c1 6387   + caddc 6389   - cmin 6445   <_ cle 6448  RR+crp 6453   +oocpnf 6650   -oocmnf 6651  RR*cxr 6652   < clt 6653  (,)cioo 7524  topGenctg 8860

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-ioo 7528  df-bases 8863  df-topgen 8864

Copyright terms: Public domain