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 30031
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 21183 . . . 4 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . 3 (𝜑𝐽 ∈ Top)
4 qtophaus.2 . . . 4 (𝜑𝐹:𝑋onto𝑌)
5 fofn 6155 . . . 4 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
64, 5syl 17 . . 3 (𝜑𝐹 Fn 𝑋)
7 qtophaus.x . . . 4 𝑋 = 𝐽
87qtoptop 21551 . . 3 ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
93, 6, 8syl2anc 694 . 2 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10 txtop 21420 . . . 4 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
119, 9, 10syl2anc 694 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12 idssxp 6047 . . . 4 ( I ↾ (𝐽 qTop 𝐹)) ⊆ ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹))
13 eqid 2651 . . . . . 6 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
1413, 13txuni 21443 . . . . 5 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
159, 9, 14syl2anc 694 . . . 4 (𝜑 → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
1612, 15syl5sseq 3686 . . 3 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
177qtopuni 21553 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐹:𝑋onto𝑌) → 𝑌 = (𝐽 qTop 𝐹))
183, 4, 17syl2anc 694 . . . . . . 7 (𝜑𝑌 = (𝐽 qTop 𝐹))
1918sqxpeqd 5175 . . . . . 6 (𝜑 → (𝑌 × 𝑌) = ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)))
2019, 15eqtr2d 2686 . . . . 5 (𝜑 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
2118eqcomd 2657 . . . . . 6 (𝜑 (𝐽 qTop 𝐹) = 𝑌)
2221reseq2d 5428 . . . . 5 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
2320, 22difeq12d 3762 . . . 4 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24 simp-4r 824 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥𝑋)
25 simplr 807 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑦𝑋)
26 opelxpi 5182 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
2724, 25, 26syl2anc 694 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
28 df-br 4686 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
2927, 28sylibr 224 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
30 simpllr 815 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) = 𝑎)
31 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑦) = 𝑏)
3230, 31opeq12d 4441 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨𝑎, 𝑏⟩)
33 simp-5r 826 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
34 simp-8r 832 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
3533, 34eqeltrrd 2731 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
3632, 35eqeltrd 2730 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
37 relxp 5160 . . . . . . . . . . . . . . . . . 18 Rel (𝑌 × 𝑌)
38 opeldifid 29538 . . . . . . . . . . . . . . . . . 18 (Rel (𝑌 × 𝑌) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦))))
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4036, 39sylib 208 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4140simprd 478 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) ≠ (𝐹𝑦))
426ad8antr 785 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝐹 Fn 𝑋)
43 qtophaus.e . . . . . . . . . . . . . . . . . 18 = (𝐹𝐹)
4443fcoinvbr 29545 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑋𝑥𝑋𝑦𝑋) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
4542, 24, 25, 44syl3anc 1366 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
4645necon3bbid 2860 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
4741, 46mpbird 247 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ¬ 𝑥 𝑦)
48 df-br 4686 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
49 brdif 4738 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5048, 49bitr3i 266 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5129, 47, 50sylanbrc 699 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
52 qtophaus.h . . . . . . . . . . . . . . 15 𝐻 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5352, 24, 25fvproj 30027 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5432, 53, 333eqtr4d 2695 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
55 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
5655eqeq1d 2653 . . . . . . . . . . . . . 14 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
5756rspcev 3340 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
5851, 54, 57syl2anc 694 . . . . . . . . . . . 12 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
59 fofun 6154 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌 → Fun 𝐹)
604, 59syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐹)
6160ad4antr 769 . . . . . . . . . . . . . 14 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
6261ad2antrr 762 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → Fun 𝐹)
63 simp-4r 824 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏𝑌)
64 foima 6158 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌 → (𝐹𝑋) = 𝑌)
654, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑋) = 𝑌)
6665ad4antr 769 . . . . . . . . . . . . . . 15 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹𝑋) = 𝑌)
6766ad2antrr 762 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → (𝐹𝑋) = 𝑌)
6863, 67eleqtrrd 2733 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏 ∈ (𝐹𝑋))
69 fvelima 6287 . . . . . . . . . . . . 13 ((Fun 𝐹𝑏 ∈ (𝐹𝑋)) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7062, 68, 69syl2anc 694 . . . . . . . . . . . 12 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7158, 70r19.29a 3107 . . . . . . . . . . 11 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
72 simpllr 815 . . . . . . . . . . . . 13 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎𝑌)
7372, 66eleqtrrd 2733 . . . . . . . . . . . 12 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹𝑋))
74 fvelima 6287 . . . . . . . . . . . 12 ((Fun 𝐹𝑎 ∈ (𝐹𝑋)) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
7561, 73, 74syl2anc 694 . . . . . . . . . . 11 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
7671, 75r19.29a 3107 . . . . . . . . . 10 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
77 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
7877eldifad 3619 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
79 elxp2 5166 . . . . . . . . . . 11 (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8078, 79sylib 208 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8176, 80r19.29vva 3110 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
82 simpr 476 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
8382fveq2d 6233 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
84 simp-4r 824 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = 𝑐)
85 simpllr 815 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥𝑋)
86 simplr 807 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦𝑋)
8752, 85, 86fvproj 30027 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
8883, 84, 873eqtr3d 2693 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
89 fof 6153 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
904, 89syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝑌)
9190ad5antr 773 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋𝑌)
9291, 85ffvelrnd 6400 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ∈ 𝑌)
9391, 86ffvelrnd 6400 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) ∈ 𝑌)
94 opelxp 5180 . . . . . . . . . . . . . 14 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹𝑥) ∈ 𝑌 ∧ (𝐹𝑦) ∈ 𝑌))
9592, 93, 94sylanbrc 699 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌))
96 simp-5r 826 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ))
9782, 96eqeltrrd 2731 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
9850simprbi 479 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) → ¬ 𝑥 𝑦)
9997, 98syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 𝑦)
1006ad5antr 773 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
101100, 85, 86, 44syl3anc 1366 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
102101necon3bbid 2860 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
10399, 102mpbid 222 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ≠ (𝐹𝑦))
10495, 103, 39sylanbrc 699 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
10588, 104eqeltrd 2730 . . . . . . . . . . 11 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
106 eldifi 3765 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑋 × 𝑋) ∖ ) → 𝑧 ∈ (𝑋 × 𝑋))
107106adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → 𝑧 ∈ (𝑋 × 𝑋))
108 elxp2 5166 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
109107, 108sylib 208 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
110109adantr 480 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
111105, 110r19.29vva 3110 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
112111r19.29an 3106 . . . . . . . . 9 ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
11381, 112impbida 895 . . . . . . . 8 (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
114 opex 4962 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
11552, 114fnmpt2i 7284 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑋)
116 difss 3770 . . . . . . . . 9 ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)
117 fvelimab 6292 . . . . . . . . 9 ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
118115, 116, 117mp2an 708 . . . . . . . 8 (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
119113, 118syl6rbbr 279 . . . . . . 7 (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
120119eqrdv 2649 . . . . . 6 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ I ))
121 ssv 3658 . . . . . . 7 𝑌 ⊆ V
122 xpss2 5162 . . . . . . 7 (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
123 difres 29539 . . . . . . 7 ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
124121, 122, 123mp2b 10 . . . . . 6 ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
125120, 124syl6eqr 2703 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
1267toptopon 20770 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
1273, 126sylib 208 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
128 qtoptopon 21555 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129127, 4, 128syl2anc 694 . . . . . 6 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
130 qtophaus.3 . . . . . 6 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
131130ralrimiva 2995 . . . . . . . 8 (𝜑 → ∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
132 imaeq2 5497 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
133132eleq1d 2715 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹𝑦) ∈ (𝐽 qTop 𝐹)))
134133cbvralv 3201 . . . . . . . 8 (∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
135131, 134sylib 208 . . . . . . 7 (𝜑 → ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
136135r19.21bi 2961 . . . . . 6 ((𝜑𝑦𝐽) → (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
1377, 7txuni 21443 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
1383, 3, 137syl2anc 694 . . . . . . . 8 (𝜑 → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
139138difeq1d 3760 . . . . . . 7 (𝜑 → ((𝑋 × 𝑋) ∖ ) = ( (𝐽 ×t 𝐽) ∖ ))
140 qtophaus.4 . . . . . . . 8 (𝜑 ∈ (Clsd‘(𝐽 ×t 𝐽)))
141 txtop 21420 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
1423, 3, 141syl2anc 694 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
143 fcoinver 29544 . . . . . . . . . . . . 13 (𝐹 Fn 𝑋 → (𝐹𝐹) Er 𝑋)
1446, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) Er 𝑋)
145 ereq1 7794 . . . . . . . . . . . . 13 ( = (𝐹𝐹) → ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋))
14643, 145ax-mp 5 . . . . . . . . . . . 12 ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋)
147144, 146sylibr 224 . . . . . . . . . . 11 (𝜑 Er 𝑋)
148 erssxp 7810 . . . . . . . . . . 11 ( Er 𝑋 ⊆ (𝑋 × 𝑋))
149147, 148syl 17 . . . . . . . . . 10 (𝜑 ⊆ (𝑋 × 𝑋))
150149, 138sseqtrd 3674 . . . . . . . . 9 (𝜑 (𝐽 ×t 𝐽))
151 eqid 2651 . . . . . . . . . 10 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
152151iscld2 20880 . . . . . . . . 9 (((𝐽 ×t 𝐽) ∈ Top ∧ (𝐽 ×t 𝐽)) → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
153142, 150, 152syl2anc 694 . . . . . . . 8 (𝜑 → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
154140, 153mpbid 222 . . . . . . 7 (𝜑 → ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽))
155139, 154eqeltrd 2730 . . . . . 6 (𝜑 → ((𝑋 × 𝑋) ∖ ) ∈ (𝐽 ×t 𝐽))
15690, 90, 127, 127, 129, 129, 130, 136, 155, 52txomap 30029 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157125, 156eqeltrrd 2731 . . . 4 (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15823, 157eqeltrd 2730 . . 3 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
159 eqid 2651 . . . . 5 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
160159iscld2 20880 . . . 4 ((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → (( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ↔ ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
161160biimpar 501 . . 3 (((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ∧ ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
16211, 16, 158, 161syl21anc 1365 . 2 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
16313hausdiag 21496 . 2 ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
1649, 162, 163sylanbrc 699 1 (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  wss 3607  cop 4216   cuni 4468   class class class wbr 4685   I cid 5052   × cxp 5141  ccnv 5142  cres 5145  cima 5146  ccom 5147  Rel wrel 5148  Fun wfun 5920   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  cmpt2 6692   Er wer 7784   qTop cqtop 16210  Topctop 20746  TopOnctopon 20763  Clsdccld 20868  Hauscha 21160   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-er 7787  df-topgen 16151  df-qtop 16214  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-haus 21167  df-tx 21413
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator