Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  qtophaus Structured version   Visualization version   GIF version

Theorem qtophaus 33835
Description: If an open map's graph in the product space (𝐽 ×t 𝐽) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.)
Hypotheses
Ref Expression
qtophaus.x 𝑋 = 𝐽
qtophaus.e = (𝐹𝐹)
qtophaus.h 𝐻 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
qtophaus.1 (𝜑𝐽 ∈ Haus)
qtophaus.2 (𝜑𝐹:𝑋onto𝑌)
qtophaus.3 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
qtophaus.4 (𝜑 ∈ (Clsd‘(𝐽 ×t 𝐽)))
Assertion
Ref Expression
qtophaus (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)
Distinct variable groups:   𝑥, ,𝑦   𝑥,𝐹,𝑦   𝑥,𝐻,𝑦   𝑥,𝐽,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝜑,𝑥,𝑦

Proof of Theorem qtophaus
Dummy variables 𝑎 𝑏 𝑐 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qtophaus.1 . . . 4 (𝜑𝐽 ∈ Haus)
2 haustop 23339 . . . 4 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . 3 (𝜑𝐽 ∈ Top)
4 qtophaus.2 . . . 4 (𝜑𝐹:𝑋onto𝑌)
5 fofn 6822 . . . 4 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
64, 5syl 17 . . 3 (𝜑𝐹 Fn 𝑋)
7 qtophaus.x . . . 4 𝑋 = 𝐽
87qtoptop 23708 . . 3 ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
93, 6, 8syl2anc 584 . 2 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10 txtop 23577 . . . 4 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
119, 9, 10syl2anc 584 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12 idssxp 6067 . . . 4 ( I ↾ (𝐽 qTop 𝐹)) ⊆ ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹))
13 eqid 2737 . . . . . 6 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
1413, 13txuni 23600 . . . . 5 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
159, 9, 14syl2anc 584 . . . 4 (𝜑 → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
1612, 15sseqtrid 4026 . . 3 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
177qtopuni 23710 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐹:𝑋onto𝑌) → 𝑌 = (𝐽 qTop 𝐹))
183, 4, 17syl2anc 584 . . . . . . 7 (𝜑𝑌 = (𝐽 qTop 𝐹))
1918sqxpeqd 5717 . . . . . 6 (𝜑 → (𝑌 × 𝑌) = ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)))
2019, 15eqtr2d 2778 . . . . 5 (𝜑 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
2118eqcomd 2743 . . . . . 6 (𝜑 (𝐽 qTop 𝐹) = 𝑌)
2221reseq2d 5997 . . . . 5 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
2320, 22difeq12d 4127 . . . 4 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24 qtophaus.h . . . . . . . . . 10 𝐻 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
25 opex 5469 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
2624, 25fnmpoi 8095 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑋)
27 difss 4136 . . . . . . . . 9 ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)
28 fvelimab 6981 . . . . . . . . 9 ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
2926, 27, 28mp2an 692 . . . . . . . 8 (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
30 simp-4r 784 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥𝑋)
31 simplr 769 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑦𝑋)
32 opelxpi 5722 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
3330, 31, 32syl2anc 584 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
34 df-br 5144 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
3533, 34sylibr 234 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
36 simpllr 776 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) = 𝑎)
37 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑦) = 𝑏)
3836, 37opeq12d 4881 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨𝑎, 𝑏⟩)
39 simp-5r 786 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
40 simp-8r 792 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
4139, 40eqeltrrd 2842 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
4238, 41eqeltrd 2841 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
43 relxp 5703 . . . . . . . . . . . . . . . . . 18 Rel (𝑌 × 𝑌)
44 opeldifid 32612 . . . . . . . . . . . . . . . . . 18 (Rel (𝑌 × 𝑌) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦))))
4543, 44ax-mp 5 . . . . . . . . . . . . . . . . 17 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4642, 45sylib 218 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4746simprd 495 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) ≠ (𝐹𝑦))
486ad8antr 740 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝐹 Fn 𝑋)
49 qtophaus.e . . . . . . . . . . . . . . . . . 18 = (𝐹𝐹)
5049fcoinvbr 32618 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑋𝑥𝑋𝑦𝑋) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
5148, 30, 31, 50syl3anc 1373 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
5251necon3bbid 2978 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
5347, 52mpbird 257 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ¬ 𝑥 𝑦)
54 df-br 5144 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
55 brdif 5196 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5654, 55bitr3i 277 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5735, 53, 56sylanbrc 583 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
5824, 30, 31fvproj 8159 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5938, 58, 393eqtr4d 2787 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
60 fveqeq2 6915 . . . . . . . . . . . . . 14 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
6160rspcev 3622 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
6257, 59, 61syl2anc 584 . . . . . . . . . . . 12 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
63 fofun 6821 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌 → Fun 𝐹)
644, 63syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐹)
6564ad4antr 732 . . . . . . . . . . . . . 14 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
6665ad2antrr 726 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → Fun 𝐹)
67 simp-4r 784 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏𝑌)
68 foima 6825 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌 → (𝐹𝑋) = 𝑌)
694, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑋) = 𝑌)
7069ad4antr 732 . . . . . . . . . . . . . . 15 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹𝑋) = 𝑌)
7170ad2antrr 726 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → (𝐹𝑋) = 𝑌)
7267, 71eleqtrrd 2844 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏 ∈ (𝐹𝑋))
73 fvelima 6974 . . . . . . . . . . . . 13 ((Fun 𝐹𝑏 ∈ (𝐹𝑋)) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7466, 72, 73syl2anc 584 . . . . . . . . . . . 12 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7562, 74r19.29a 3162 . . . . . . . . . . 11 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
76 simpllr 776 . . . . . . . . . . . . 13 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎𝑌)
7776, 70eleqtrrd 2844 . . . . . . . . . . . 12 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹𝑋))
78 fvelima 6974 . . . . . . . . . . . 12 ((Fun 𝐹𝑎 ∈ (𝐹𝑋)) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
7965, 77, 78syl2anc 584 . . . . . . . . . . 11 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
8075, 79r19.29a 3162 . . . . . . . . . 10 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
81 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
8281eldifad 3963 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
83 elxp2 5709 . . . . . . . . . . 11 (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8482, 83sylib 218 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8580, 84r19.29vva 3216 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
86 simpr 484 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
8786fveq2d 6910 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
88 simp-4r 784 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = 𝑐)
89 simpllr 776 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥𝑋)
90 simplr 769 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦𝑋)
9124, 89, 90fvproj 8159 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
9287, 88, 913eqtr3d 2785 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
93 fof 6820 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
944, 93syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝑌)
9594ad5antr 734 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋𝑌)
9695, 89ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ∈ 𝑌)
9795, 90ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) ∈ 𝑌)
98 opelxp 5721 . . . . . . . . . . . . . 14 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹𝑥) ∈ 𝑌 ∧ (𝐹𝑦) ∈ 𝑌))
9996, 97, 98sylanbrc 583 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌))
100 simp-5r 786 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ))
10186, 100eqeltrrd 2842 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
10256simprbi 496 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) → ¬ 𝑥 𝑦)
103101, 102syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 𝑦)
1046ad5antr 734 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
105104, 89, 90, 50syl3anc 1373 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
106105necon3bbid 2978 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
107103, 106mpbid 232 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ≠ (𝐹𝑦))
10899, 107, 45sylanbrc 583 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
10992, 108eqeltrd 2841 . . . . . . . . . . 11 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
110 eldifi 4131 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑋 × 𝑋) ∖ ) → 𝑧 ∈ (𝑋 × 𝑋))
111110adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → 𝑧 ∈ (𝑋 × 𝑋))
112 elxp2 5709 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
113111, 112sylib 218 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
114113adantr 480 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
115109, 114r19.29vva 3216 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
116115r19.29an 3158 . . . . . . . . 9 ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
11785, 116impbida 801 . . . . . . . 8 (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
11829, 117bitr4id 290 . . . . . . 7 (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119118eqrdv 2735 . . . . . 6 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ I ))
120 ssv 4008 . . . . . . 7 𝑌 ⊆ V
121 xpss2 5705 . . . . . . 7 (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122 difres 32613 . . . . . . 7 ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123120, 121, 122mp2b 10 . . . . . 6 ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124119, 123eqtr4di 2795 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
1257toptopon 22923 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
1263, 125sylib 218 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
127 qtoptopon 23712 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128126, 4, 127syl2anc 584 . . . . . 6 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129 qtophaus.3 . . . . . 6 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
130129ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
131 imaeq2 6074 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
132131eleq1d 2826 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹𝑦) ∈ (𝐽 qTop 𝐹)))
133132cbvralvw 3237 . . . . . . . 8 (∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
134130, 133sylib 218 . . . . . . 7 (𝜑 → ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
135134r19.21bi 3251 . . . . . 6 ((𝜑𝑦𝐽) → (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
1367, 7txuni 23600 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
1373, 3, 136syl2anc 584 . . . . . . . 8 (𝜑 → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
138137difeq1d 4125 . . . . . . 7 (𝜑 → ((𝑋 × 𝑋) ∖ ) = ( (𝐽 ×t 𝐽) ∖ ))
139 qtophaus.4 . . . . . . . 8 (𝜑 ∈ (Clsd‘(𝐽 ×t 𝐽)))
140 txtop 23577 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
1413, 3, 140syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142 fcoinver 32617 . . . . . . . . . . . . 13 (𝐹 Fn 𝑋 → (𝐹𝐹) Er 𝑋)
1436, 142syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) Er 𝑋)
144 ereq1 8752 . . . . . . . . . . . . 13 ( = (𝐹𝐹) → ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋))
14549, 144ax-mp 5 . . . . . . . . . . . 12 ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋)
146143, 145sylibr 234 . . . . . . . . . . 11 (𝜑 Er 𝑋)
147 erssxp 8768 . . . . . . . . . . 11 ( Er 𝑋 ⊆ (𝑋 × 𝑋))
148146, 147syl 17 . . . . . . . . . 10 (𝜑 ⊆ (𝑋 × 𝑋))
149148, 137sseqtrd 4020 . . . . . . . . 9 (𝜑 (𝐽 ×t 𝐽))
150 eqid 2737 . . . . . . . . . 10 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
151150iscld2 23036 . . . . . . . . 9 (((𝐽 ×t 𝐽) ∈ Top ∧ (𝐽 ×t 𝐽)) → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
152141, 149, 151syl2anc 584 . . . . . . . 8 (𝜑 → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
153139, 152mpbid 232 . . . . . . 7 (𝜑 → ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽))
154138, 153eqeltrd 2841 . . . . . 6 (𝜑 → ((𝑋 × 𝑋) ∖ ) ∈ (𝐽 ×t 𝐽))
15594, 94, 126, 126, 128, 128, 129, 135, 154, 24txomap 33833 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156124, 155eqeltrrd 2842 . . . 4 (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15723, 156eqeltrd 2841 . . 3 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158 eqid 2737 . . . . 5 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159158iscld2 23036 . . . 4 ((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → (( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ↔ ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
160159biimpar 477 . . 3 (((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ∧ ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
16111, 16, 157, 160syl21anc 838 . 2 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
16213hausdiag 23653 . 2 ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
1639, 161, 162sylanbrc 583 1 (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  wss 3951  cop 4632   cuni 4907   class class class wbr 5143   I cid 5577   × cxp 5683  ccnv 5684  cres 5687  cima 5688  ccom 5689  Rel wrel 5690  Fun wfun 6555   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561  (class class class)co 7431  cmpo 7433   Er wer 8742   qTop cqtop 17548  Topctop 22899  TopOnctopon 22916  Clsdccld 23024  Hauscha 23316   ×t ctx 23568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-er 8745  df-topgen 17488  df-qtop 17552  df-top 22900  df-topon 22917  df-bases 22953  df-cld 23027  df-haus 23323  df-tx 23570
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator