Theorem eltopsp 7583

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 7585, 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 2617	. . . 4 |- (U.JTopSpJ <-> <.U.J, J>. e. TopSp)
2		relopab 3263	. . . . . 6 |- Rel {<.x, y>. | (y e. Top /\ x = U.y)}
3		df-topsp 7572	. . . . . . 7 |- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}
4	3	releqi 3241	. . . . . 6 |- (Rel TopSp <-> Rel {<.x, y>. | (y e. Top /\ x = U.y)})
5	2, 4	mpbir 190	. . . . 5 |- Rel TopSp
6	5	brrelexi 3205	. . . 4 |- (U.JTopSpJ -> U.J e. V)
7	1, 6	sylbir 201	. . 3 |- (<.U.J, J>. e. TopSp -> U.J e. V)
8		uniexb 2904	. . . 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 2868	. . 3 |- (J e. Top -> U.J e. V)
12		elisset 1815	. . 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 1480	. . . . 5 |- (x = U.J -> (x = U.y <-> U.J = U.y))
15	14	anbi2d 615	. . . 4 |- (x = U.J -> ((y e. Top /\ x = U.y) <-> (y e. Top /\ U.J = U.y)))
16		eleq1 1533	. . . . 5 |- (y = J -> (y e. Top <-> J e. Top))
17		unieq 2507	. . . . . 6 |- (y = J -> U.y = U.J)
18	17	eqeq2d 1485	. . . . 5 |- (y = J -> (U.J = U.y <-> U.J = U.J))
19	16, 18	anbi12d 627	. . . 4 |- (y = J -> ((y e. Top /\ U.J = U.y) <-> (J e. Top /\ U.J = U.J)))
20	15, 19	opelopabg 2814	. . 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 1537	. . 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 723	. . 3 |- (J e. Top <-> (J e. Top /\ U.J = U.J))
24	20, 21, 23	3bitr4g 554	. 2 |- ((U.J e. V /\ J e. V) -> (<.U.J, J>. e. TopSp <-> J e. Top))
25	10, 13, 24	pm5.21nii 678	1 |- (<.U.J, J>. e. TopSp <-> J e. Top)

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957  Vcvv 1809  <.cop 2409  U.cuni 2500   class class class wbr 2616  {copab 2663  Rel wrel 3172  Topctop 7567  TopSpctps 7568

This theorem is referenced by:  indistps 7632  distps 7633

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-pr 2776  ax-un 2863

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-xp 3181  df-rel 3182  df-topsp 7572

Copyright terms: Public domain