MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  epttop Structured version   Visualization version   GIF version

Theorem epttop 21324
Description: The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
epttop ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑃
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem epttop
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab 3941 . . . . 5 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ↔ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴)))
2 eleq2 2854 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃 𝑦))
3 eqeq1 2782 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝐴 𝑦 = 𝐴))
42, 3imbi12d 337 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = 𝐴) ↔ (𝑃 𝑦 𝑦 = 𝐴)))
5 simprl 758 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → 𝑦 ⊆ 𝒫 𝐴)
6 sspwuni 4889 . . . . . . . . 9 (𝑦 ⊆ 𝒫 𝐴 𝑦𝐴)
75, 6sylib 210 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → 𝑦𝐴)
8 vuniex 7286 . . . . . . . . 9 𝑦 ∈ V
98elpw 4429 . . . . . . . 8 ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴)
107, 9sylibr 226 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → 𝑦 ∈ 𝒫 𝐴)
11 eluni2 4717 . . . . . . . . . 10 (𝑃 𝑦 ↔ ∃𝑥𝑦 𝑃𝑥)
12 r19.29 3200 . . . . . . . . . . . . 13 ((∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴) ∧ ∃𝑥𝑦 𝑃𝑥) → ∃𝑥𝑦 ((𝑃𝑥𝑥 = 𝐴) ∧ 𝑃𝑥))
13 simpr 477 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ (𝑃𝑥𝑥 = 𝐴)) → (𝑃𝑥𝑥 = 𝐴))
1413impr 447 . . . . . . . . . . . . . . 15 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = 𝐴) ∧ 𝑃𝑥)) → 𝑥 = 𝐴)
15 elssuni 4742 . . . . . . . . . . . . . . . 16 (𝑥𝑦𝑥 𝑦)
1615adantr 473 . . . . . . . . . . . . . . 15 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = 𝐴) ∧ 𝑃𝑥)) → 𝑥 𝑦)
1714, 16eqsstr3d 3898 . . . . . . . . . . . . . 14 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = 𝐴) ∧ 𝑃𝑥)) → 𝐴 𝑦)
1817rexlimiva 3226 . . . . . . . . . . . . 13 (∃𝑥𝑦 ((𝑃𝑥𝑥 = 𝐴) ∧ 𝑃𝑥) → 𝐴 𝑦)
1912, 18syl 17 . . . . . . . . . . . 12 ((∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴) ∧ ∃𝑥𝑦 𝑃𝑥) → 𝐴 𝑦)
2019ex 405 . . . . . . . . . . 11 (∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴) → (∃𝑥𝑦 𝑃𝑥𝐴 𝑦))
2120ad2antll 716 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → (∃𝑥𝑦 𝑃𝑥𝐴 𝑦))
2211, 21syl5bi 234 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → (𝑃 𝑦𝐴 𝑦))
2322, 7jctild 518 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → (𝑃 𝑦 → ( 𝑦𝐴𝐴 𝑦)))
24 eqss 3875 . . . . . . . 8 ( 𝑦 = 𝐴 ↔ ( 𝑦𝐴𝐴 𝑦))
2523, 24syl6ibr 244 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → (𝑃 𝑦 𝑦 = 𝐴))
264, 10, 25elrabd 3598 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴))) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
2726ex 405 . . . . 5 ((𝐴𝑉𝑃𝐴) → ((𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = 𝐴)) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}))
281, 27syl5bi 234 . . . 4 ((𝐴𝑉𝑃𝐴) → (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}))
2928alrimiv 1886 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}))
30 inss1 4094 . . . . . . . . 9 (𝑦𝑧) ⊆ 𝑦
31 simprll 766 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → 𝑦 ∈ 𝒫 𝐴)
3231elpwid 4435 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → 𝑦𝐴)
3330, 32syl5ss 3871 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → (𝑦𝑧) ⊆ 𝐴)
34 vex 3418 . . . . . . . . . 10 𝑦 ∈ V
3534inex1 5079 . . . . . . . . 9 (𝑦𝑧) ∈ V
3635elpw 4429 . . . . . . . 8 ((𝑦𝑧) ∈ 𝒫 𝐴 ↔ (𝑦𝑧) ⊆ 𝐴)
3733, 36sylibr 226 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → (𝑦𝑧) ∈ 𝒫 𝐴)
38 elin 4059 . . . . . . . 8 (𝑃 ∈ (𝑦𝑧) ↔ (𝑃𝑦𝑃𝑧))
39 simprlr 767 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → (𝑃𝑦𝑦 = 𝐴))
40 simprrr 769 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → (𝑃𝑧𝑧 = 𝐴))
4139, 40anim12d 599 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → ((𝑃𝑦𝑃𝑧) → (𝑦 = 𝐴𝑧 = 𝐴)))
42 ineq12 4073 . . . . . . . . . 10 ((𝑦 = 𝐴𝑧 = 𝐴) → (𝑦𝑧) = (𝐴𝐴))
43 inidm 4084 . . . . . . . . . 10 (𝐴𝐴) = 𝐴
4442, 43syl6eq 2830 . . . . . . . . 9 ((𝑦 = 𝐴𝑧 = 𝐴) → (𝑦𝑧) = 𝐴)
4541, 44syl6 35 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → ((𝑃𝑦𝑃𝑧) → (𝑦𝑧) = 𝐴))
4638, 45syl5bi 234 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → (𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = 𝐴))
4737, 46jca 504 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))) → ((𝑦𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = 𝐴)))
4847ex 405 . . . . 5 ((𝐴𝑉𝑃𝐴) → (((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴))) → ((𝑦𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = 𝐴))))
49 eleq2 2854 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃𝑦))
50 eqeq1 2782 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
5149, 50imbi12d 337 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = 𝐴) ↔ (𝑃𝑦𝑦 = 𝐴)))
5251elrab 3595 . . . . . 6 (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)))
53 eleq2 2854 . . . . . . . 8 (𝑥 = 𝑧 → (𝑃𝑥𝑃𝑧))
54 eqeq1 2782 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝐴𝑧 = 𝐴))
5553, 54imbi12d 337 . . . . . . 7 (𝑥 = 𝑧 → ((𝑃𝑥𝑥 = 𝐴) ↔ (𝑃𝑧𝑧 = 𝐴)))
5655elrab 3595 . . . . . 6 (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴)))
5752, 56anbi12i 617 . . . . 5 ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = 𝐴))))
58 eleq2 2854 . . . . . . 7 (𝑥 = (𝑦𝑧) → (𝑃𝑥𝑃 ∈ (𝑦𝑧)))
59 eqeq1 2782 . . . . . . 7 (𝑥 = (𝑦𝑧) → (𝑥 = 𝐴 ↔ (𝑦𝑧) = 𝐴))
6058, 59imbi12d 337 . . . . . 6 (𝑥 = (𝑦𝑧) → ((𝑃𝑥𝑥 = 𝐴) ↔ (𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = 𝐴)))
6160elrab 3595 . . . . 5 ((𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ↔ ((𝑦𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = 𝐴)))
6248, 57, 613imtr4g 288 . . . 4 ((𝐴𝑉𝑃𝐴) → ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}))
6362ralrimivv 3140 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
64 pwexg 5133 . . . . . 6 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
6564adantr 473 . . . . 5 ((𝐴𝑉𝑃𝐴) → 𝒫 𝐴 ∈ V)
66 rabexg 5091 . . . . 5 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ V)
6765, 66syl 17 . . . 4 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ V)
68 istopg 21210 . . . 4 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})))
6967, 68syl 17 . . 3 ((𝐴𝑉𝑃𝐴) → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})))
7029, 63, 69mpbir2and 700 . 2 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ Top)
71 eleq2 2854 . . . . . 6 (𝑥 = 𝐴 → (𝑃𝑥𝑃𝐴))
72 eqeq1 2782 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = 𝐴𝐴 = 𝐴))
7371, 72imbi12d 337 . . . . 5 (𝑥 = 𝐴 → ((𝑃𝑥𝑥 = 𝐴) ↔ (𝑃𝐴𝐴 = 𝐴)))
74 pwidg 4438 . . . . . 6 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
7574adantr 473 . . . . 5 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ 𝒫 𝐴)
76 eqidd 2779 . . . . . 6 ((𝐴𝑉𝑃𝐴) → 𝐴 = 𝐴)
7776a1d 25 . . . . 5 ((𝐴𝑉𝑃𝐴) → (𝑃𝐴𝐴 = 𝐴))
7873, 75, 77elrabd 3598 . . . 4 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
79 elssuni 4742 . . . 4 (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
8078, 79syl 17 . . 3 ((𝐴𝑉𝑃𝐴) → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
81 ssrab2 3948 . . . . 5 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ⊆ 𝒫 𝐴
82 sspwuni 4889 . . . . 5 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ⊆ 𝒫 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ⊆ 𝐴)
8381, 82mpbi 222 . . . 4 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ⊆ 𝐴
8483a1i 11 . . 3 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ⊆ 𝐴)
8580, 84eqssd 3877 . 2 ((𝐴𝑉𝑃𝐴) → 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)})
86 istopon 21227 . 2 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ Top ∧ 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)}))
8770, 85, 86sylanbrc 575 1 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  wal 1505   = wceq 1507  wcel 2050  wral 3088  wrex 3089  {crab 3092  Vcvv 3415  cin 3830  wss 3831  𝒫 cpw 4423   cuni 4713  cfv 6190  Topctop 21208  TopOnctopon 21225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-iota 6154  df-fun 6192  df-fv 6198  df-top 21209  df-topon 21226
This theorem is referenced by:  dfac14lem  21932  dfac14  21933
  Copyright terms: Public domain W3C validator