Theorem retopbas 7652

Description: A basis for the standard topology on the reals.

Assertion

Ref	Expression
retopbas	|- ran (,) e. Bases

Proof of Theorem retopbas

Step	Hyp	Ref	Expression
1		eleq2 1538	. . . . . . 7 |- (w = (x i^i y) -> (z e. w <-> z e. (x i^i y)))
2		sseq1 2085	. . . . . . 7 |- (w = (x i^i y) -> (w (_ (x i^i y) <-> (x i^i y) (_ (x i^i y)))
3	1, 2	anbi12d 630	. . . . . 6 |- (w = (x i^i y) -> ((z e. w /\ w (_ (x i^i y)) <-> (z e. (x i^i y) /\ (x i^i y) (_ (x i^i y))))
4	3	rcla4ev 1880	. . . . 5 |- (((x i^i y) e. ran (,) /\ (z e. (x i^i y) /\ (x i^i y) (_ (x i^i y))) -> E.w e. ran (,)(z e. w /\ w (_ (x i^i y)))
5		opreq1 3974	. . . . . . . . . . . . . . . . . . 19 |- (t = if(z <_ v, v, z) -> (t(,)f) = (if(z <_ v, v, z)(,)f))
6	5	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 |- (t = if(z <_ v, v, z) -> ((t(,)f) = (x i^i y) <-> (if(z <_ v, v, z)(,)f) = (x i^i y)))
7		opreq2 3975	. . . . . . . . . . . . . . . . . . 19 |- (f = if(w <_ u, w, u) -> (if(z <_ v, v, z)(,)f) = (if(z <_ v, v, z)(,)if(w <_ u, w, u)))
8	7	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 |- (f = if(w <_ u, w, u) -> ((if(z <_ v, v, z)(,)f) = (x i^i y) <-> (if(z <_ v, v, z)(,)if(w <_ u, w, u)) = (x i^i y)))
9	6, 8	rcla42ev 1884	. . . . . . . . . . . . . . . . 17 |- ((if(z <_ v, v, z) e. RR* /\ if(w <_ u, w, u) e. RR* /\ (if(z <_ v, v, z)(,)if(w <_ u, w, u)) = (x i^i y)) -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))
10		ifcl 2384	. . . . . . . . . . . . . . . . . . 19 |- ((v e. RR* /\ z e. RR*) -> if(z <_ v, v, z) e. RR*)
11	10	ad2ant2r 411	. . . . . . . . . . . . . . . . . 18 |- (((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) -> if(z <_ v, v, z) e. RR*)
12	11	adantr 391	. . . . . . . . . . . . . . . . 17 |- ((((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) /\ ((z(,)w) = x /\ (v(,)u) = y)) -> if(z <_ v, v, z) e. RR*)
13		ifcl 2384	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. RR* /\ u e. RR*) -> if(w <_ u, w, u) e. RR*)
14	13	ancoms 438	. . . . . . . . . . . . . . . . . . 19 |- ((u e. RR* /\ w e. RR*) -> if(w <_ u, w, u) e. RR*)
15	14	ad2ant2l 410	. . . . . . . . . . . . . . . . . 18 |- (((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) -> if(w <_ u, w, u) e. RR*)
16	15	adantr 391	. . . . . . . . . . . . . . . . 17 |- ((((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) /\ ((z(,)w) = x /\ (v(,)u) = y)) -> if(w <_ u, w, u) e. RR*)
17		iooint 6373	. . . . . . . . . . . . . . . . . . 19 |- (((z e. RR* /\ w e. RR*) /\ (v e. RR* /\ u e. RR*)) -> ((z(,)w) i^i (v(,)u)) = (if(z <_ v, v, z)(,)if(w <_ u, w, u)))
18	17	ancoms 438	. . . . . . . . . . . . . . . . . 18 |- (((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) -> ((z(,)w) i^i (v(,)u)) = (if(z <_ v, v, z)(,)if(w <_ u, w, u)))
19		ineq12 2215	. . . . . . . . . . . . . . . . . 18 |- (((z(,)w) = x /\ (v(,)u) = y) -> ((z(,)w) i^i (v(,)u)) = (x i^i y))
20	18, 19	sylan9req 1531	. . . . . . . . . . . . . . . . 17 |- ((((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) /\ ((z(,)w) = x /\ (v(,)u) = y)) -> (if(z <_ v, v, z)(,)if(w <_ u, w, u)) = (x i^i y))
21	9, 12, 16, 20	syl3anc 860	. . . . . . . . . . . . . . . 16 |- ((((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) /\ ((z(,)w) = x /\ (v(,)u) = y)) -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))
22	21	exp32 379	. . . . . . . . . . . . . . 15 |- (((v e. RR* /\ u e. RR*) /\ (z e. RR* /\ w e. RR*)) -> ((z(,)w) = x -> ((v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))))
23	22	exp31 378	. . . . . . . . . . . . . 14 |- (v e. RR* -> (u e. RR* -> ((z e. RR* /\ w e. RR*) -> ((z(,)w) = x -> ((v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))))))
24	23	com4t 40	. . . . . . . . . . . . 13 |- ((z e. RR* /\ w e. RR*) -> ((z(,)w) = x -> (v e. RR* -> (u e. RR* -> ((v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))))))
25	24	imp31 362	. . . . . . . . . . . 12 |- ((((z e. RR* /\ w e. RR*) /\ (z(,)w) = x) /\ v e. RR*) -> (u e. RR* -> ((v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))))
26	25	r19.23adv 1749	. . . . . . . . . . 11 |- ((((z e. RR* /\ w e. RR*) /\ (z(,)w) = x) /\ v e. RR*) -> (E.u e. RR* (v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y)))
27	26	r19.23adva 1750	. . . . . . . . . 10 |- (((z e. RR* /\ w e. RR*) /\ (z(,)w) = x) -> (E.v e. RR* E.u e. RR* (v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y)))
28	27	exp31 378	. . . . . . . . 9 |- (z e. RR* -> (w e. RR* -> ((z(,)w) = x -> (E.v e. RR* E.u e. RR* (v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y)))))
29	28	r19.23adv 1749	. . . . . . . 8 |- (z e. RR* -> (E.w e. RR* (z(,)w) = x -> (E.v e. RR* E.u e. RR* (v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))))
30	29	r19.23aiv 1746	. . . . . . 7 |- (E.z e. RR* E.w e. RR* (z(,)w) = x -> (E.v e. RR* E.u e. RR* (v(,)u) = y -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y)))
31	30	imp 350	. . . . . 6 |- ((E.z e. RR* E.w e. RR* (z(,)w) = x /\ E.v e. RR* E.u e. RR* (v(,)u) = y) -> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))
32		ioof 6401	. . . . . . . 8 |- (,):(RR* X. RR*)-->P~RR
33		ffn 3633	. . . . . . . 8 |- ((,):(RR* X. RR*)-->P~RR -> (,) Fn (RR* X. RR*))
34	32, 33	ax-mp 7	. . . . . . 7 |- (,) Fn (RR* X. RR*)
35		oprvalelrn 4045	. . . . . . . 8 |- ((,) Fn (RR* X. RR*) -> (x e. ran (,) <-> E.z e. RR* E.w e. RR* (z(,)w) = x))
36		oprvalelrn 4045	. . . . . . . 8 |- ((,) Fn (RR* X. RR*) -> (y e. ran (,) <-> E.v e. RR* E.u e. RR* (v(,)u) = y))
37	35, 36	anbi12d 630	. . . . . . 7 |- ((,) Fn (RR* X. RR*) -> ((x e. ran (,) /\ y e. ran (,)) <-> (E.z e. RR* E.w e. RR* (z(,)w) = x /\ E.v e. RR* E.u e. RR* (v(,)u) = y)))
38	34, 37	ax-mp 7	. . . . . 6 |- ((x e. ran (,) /\ y e. ran (,)) <-> (E.z e. RR* E.w e. RR* (z(,)w) = x /\ E.v e. RR* E.u e. RR* (v(,)u) = y))
39		oprvalelrn 4045	. . . . . . 7 |- ((,) Fn (RR* X. RR*) -> ((x i^i y) e. ran (,) <-> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y)))
40	34, 39	ax-mp 7	. . . . . 6 |- ((x i^i y) e. ran (,) <-> E.t e. RR* E.f e. RR* (t(,)f) = (x i^i y))
41	31, 38, 40	3imtr4 219	. . . . 5 |- ((x e. ran (,) /\ y e. ran (,)) -> (x i^i y) e. ran (,))
42		ssid 2083	. . . . . 6 |- (x i^i y) (_ (x i^i y)
43	42	jctr 291	. . . . 5 |- (z e. (x i^i y) -> (z e. (x i^i y) /\ (x i^i y) (_ (x i^i y)))
44	4, 41, 43	syl2an 456	. . . 4 |- (((x e. ran (,) /\ y e. ran (,)) /\ z e. (x i^i y)) -> E.w e. ran (,)(z e. w /\ w (_ (x i^i y)))
45	44	3impa 830	. . 3 |- ((x e. ran (,) /\ y e. ran (,) /\ z e. (x i^i y)) -> E.w e. ran (,)(z e. w /\ w (_ (x i^i y)))
46	45	rgen3 1727	. 2 |- A.x e. ran (,)A.y e. ran (,)A.z e. (x i^i y)E.w e. ran (,)(z e. w /\ w (_ (x i^i y))
47		iooex 6366	. . . 4 |- (,) e. V
48	47	rnex 3367	. . 3 |- ran (,) e. V
49		isbasis2g 7611	. . 3 |- (ran (,) e. V -> (ran (,) e. Bases <-> A.x e. ran (,)A.y e. ran (,)A.z e. (x i^i y)E.w e. ran (,)(z e. w /\ w (_