Theorem eltopsp 7604

Description: Construct a topological space from a topology and vice-versa. We say that A is a topology on U.A. (This could be proved more efficiently from istps 7606, but the proof here does not require the Axiom of Regularity.)

Assertion

Ref	Expression
eltopsp	|- (<.U.J, J>. e. TopSp <-> J e. Top)

Proof of Theorem eltopsp

Step	Hyp	Ref	Expression
1		df-br 2620	. . . 4 |- (U.JTopSpJ <-> <.U.J, J>. e. TopSp)
2		relopab 3266	. . . . . 6 |- Rel {<.x, y>. | (y e. Top /\ x = U.y)}
3		df-topsp 7593	. . . . . . 7 |- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}
4	3	releqi 3244	. . . . . 6 |- (Rel TopSp <-> Rel {<.x, y>. | (y e. Top /\ x = U.y)})
5	2, 4	mpbir 190	. . . . 5 |- Rel TopSp
6	5	brrelexi 3208	. . . 4 |- (U.JTopSpJ -> U.J e. V)
7	1, 6	sylbir 201	. . 3 |- (<.U.J, J>. e. TopSp -> U.J e. V)
8		uniexb 2907	. . . 4 |- (J e. V <-> U.J e. V)
9	7, 8	sylibr 200	. . 3 |- (<.U.J, J>. e. TopSp -> J e. V)
10	7, 9	jca 288	. 2 |- (<.U.J, J>. e. TopSp -> (U.J e. V /\ J e. V))
11		uniexg 2871	. . 3 |- (J e. Top -> U.J e. V)
12		elisset 1817	. . 3 |- (J e. Top -> J e. V)
13	11, 12	jca 288	. 2 |- (J e. Top -> (U.J e. V /\ J e. V))
14		eqeq1 1481	. . . . 5 |- (x = U.J -> (x = U.y <-> U.J = U.y))
15	14	anbi2d 616	. . . 4 |- (x = U.J -> ((y e. Top /\ x = U.y) <-> (y e. Top /\ U.J = U.y)))
16		eleq1 1534	. . . . 5 |- (y = J -> (y e. Top <-> J e. Top))
17		unieq 2510	. . . . . 6 |- (y = J -> U.y = U.J)
18	17	eqeq2d 1486	. . . . 5 |- (y = J -> (U.J = U.y <-> U.J = U.J))
19	16, 18	anbi12d 628	. . . 4 |- (y = J -> ((y e. Top /\ U.J = U.y) <-> (J e. Top /\ U.J = U.J)))
20	15, 19	opelopabg 2817	. . 3 |- ((U.J e. V /\ J e. V) -> (<.U.J, J>. e. {<.x, y>. | (y e. Top /\ x = U.y)} <-> (J e. Top /\ U.J = U.J)))
21	3	eleq2i 1538	. . 3 |- (<.U.J, J>. e. TopSp <-> <.U.J, J>. e. {<.x, y>. | (y e. Top /\ x = U.y)})
22		eqid 1475	. . . 4 |- U.J = U.J
23	22	biantru 724	. . 3 |- (J e. Top <-> (J e. Top /\ U.J = U.J))
24	20, 21, 23	3bitr4g 555	. 2 |- ((U.J e. V /\ J e. V) -> (<.U.J, J>. e. TopSp <-> J e. Top))
25	10, 13, 24	pm5.21nii 679	1 |- (<.U.J, J>. e. TopSp <-> J e. Top)

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  Vcvv 1811  <.cop 2411  U.cuni 2503   class class class wbr 2619  {copab 2666  Rel wrel 3175  Topctop 7588  TopSpctps 7589

This theorem is referenced by:  indistps 7653  distps 7654

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-rel 3185  df-topsp 7593

Copyright terms: Public domain