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 29065
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 20893 . . . 4 (𝐽 ∈ Haus → 𝐽 ∈ Top)
31, 2syl 17 . . 3 (𝜑𝐽 ∈ Top)
4 qtophaus.2 . . . 4 (𝜑𝐹:𝑋onto𝑌)
5 fofn 6015 . . . 4 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
64, 5syl 17 . . 3 (𝜑𝐹 Fn 𝑋)
7 qtophaus.x . . . 4 𝑋 = 𝐽
87qtoptop 21261 . . 3 ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
93, 6, 8syl2anc 690 . 2 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10 txtop 21130 . . . 4 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
119, 9, 10syl2anc 690 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12 idssxp 28645 . . . 4 ( I ↾ (𝐽 qTop 𝐹)) ⊆ ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹))
13 eqid 2609 . . . . . 6 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
1413, 13txuni 21153 . . . . 5 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
159, 9, 14syl2anc 690 . . . 4 (𝜑 → ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
1612, 15syl5sseq 3615 . . 3 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ⊆ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
177qtopuni 21263 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐹:𝑋onto𝑌) → 𝑌 = (𝐽 qTop 𝐹))
183, 4, 17syl2anc 690 . . . . . . 7 (𝜑𝑌 = (𝐽 qTop 𝐹))
1918sqxpeqd 5055 . . . . . 6 (𝜑 → (𝑌 × 𝑌) = ( (𝐽 qTop 𝐹) × (𝐽 qTop 𝐹)))
2019, 15eqtr2d 2644 . . . . 5 (𝜑 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
2118eqcomd 2615 . . . . . 6 (𝜑 (𝐽 qTop 𝐹) = 𝑌)
2221reseq2d 5304 . . . . 5 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
2320, 22difeq12d 3690 . . . 4 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24 simp-4r 802 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥𝑋)
25 simplr 787 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑦𝑋)
26 opelxpi 5062 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
2724, 25, 26syl2anc 690 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
28 df-br 4578 . . . . . . . . . . . . . . 15 (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
2927, 28sylibr 222 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
30 simpllr 794 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) = 𝑎)
31 simpr 475 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑦) = 𝑏)
3230, 31opeq12d 4342 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨𝑎, 𝑏⟩)
33 simp-5r 804 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
34 simp-8r 810 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
3533, 34eqeltrrd 2688 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
3632, 35eqeltrd 2687 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
37 relxp 5139 . . . . . . . . . . . . . . . . . 18 Rel (𝑌 × 𝑌)
38 opeldifid 28628 . . . . . . . . . . . . . . . . . 18 (Rel (𝑌 × 𝑌) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦))))
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4036, 39sylib 206 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹𝑥) ≠ (𝐹𝑦)))
4140simprd 477 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐹𝑥) ≠ (𝐹𝑦))
426ad8antr 771 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → 𝐹 Fn 𝑋)
43 qtophaus.e . . . . . . . . . . . . . . . . . 18 = (𝐹𝐹)
4443fcoinvbr 28633 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑋𝑥𝑋𝑦𝑋) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
4542, 24, 25, 44syl3anc 1317 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
4645necon3bbid 2818 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
4741, 46mpbird 245 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ¬ 𝑥 𝑦)
48 df-br 4578 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
49 brdif 4629 . . . . . . . . . . . . . . 15 (𝑥((𝑋 × 𝑋) ∖ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5048, 49bitr3i 264 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 𝑦))
5129, 47, 50sylanbrc 694 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
52 qtophaus.h . . . . . . . . . . . . . . 15 𝐻 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5352, 24, 25fvproj 29061 . . . . . . . . . . . . . 14 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5432, 53, 333eqtr4d 2653 . . . . . . . . . . . . 13 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
55 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
5655eqeq1d 2611 . . . . . . . . . . . . . 14 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
5756rspcev 3281 . . . . . . . . . . . . 13 ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
5851, 54, 57syl2anc 690 . . . . . . . . . . . 12 (((((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) ∧ 𝑦𝑋) ∧ (𝐹𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
59 fofun 6014 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌 → Fun 𝐹)
604, 59syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐹)
6160ad4antr 763 . . . . . . . . . . . . . 14 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
6261ad2antrr 757 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → Fun 𝐹)
63 simp-4r 802 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏𝑌)
64 foima 6018 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌 → (𝐹𝑋) = 𝑌)
654, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑋) = 𝑌)
6665ad4antr 763 . . . . . . . . . . . . . . 15 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹𝑋) = 𝑌)
6766ad2antrr 757 . . . . . . . . . . . . . 14 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → (𝐹𝑋) = 𝑌)
6863, 67eleqtrrd 2690 . . . . . . . . . . . . 13 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → 𝑏 ∈ (𝐹𝑋))
69 fvelima 6143 . . . . . . . . . . . . 13 ((Fun 𝐹𝑏 ∈ (𝐹𝑋)) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7062, 68, 69syl2anc 690 . . . . . . . . . . . 12 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑦𝑋 (𝐹𝑦) = 𝑏)
7158, 70r19.29a 3059 . . . . . . . . . . 11 (((((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥𝑋) ∧ (𝐹𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
72 simpllr 794 . . . . . . . . . . . . 13 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎𝑌)
7372, 66eleqtrrd 2690 . . . . . . . . . . . 12 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹𝑋))
74 fvelima 6143 . . . . . . . . . . . 12 ((Fun 𝐹𝑎 ∈ (𝐹𝑋)) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
7561, 73, 74syl2anc 690 . . . . . . . . . . 11 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥𝑋 (𝐹𝑥) = 𝑎)
7671, 75r19.29a 3059 . . . . . . . . . 10 (((((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎𝑌) ∧ 𝑏𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
77 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
7877eldifad 3551 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
79 elxp2 5046 . . . . . . . . . . 11 (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8078, 79sylib 206 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎𝑌𝑏𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
8176, 80r19.29vva 3061 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
82 simpr 475 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
8382fveq2d 6092 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
84 simp-4r 802 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻𝑧) = 𝑐)
85 simpllr 794 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥𝑋)
86 simplr 787 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦𝑋)
8752, 85, 86fvproj 29061 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
8883, 84, 873eqtr3d 2651 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
89 fof 6013 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
904, 89syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝑌)
9190ad5antr 765 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋𝑌)
9291, 85ffvelrnd 6253 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ∈ 𝑌)
9391, 86ffvelrnd 6253 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) ∈ 𝑌)
94 opelxp 5060 . . . . . . . . . . . . . 14 (⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹𝑥) ∈ 𝑌 ∧ (𝐹𝑦) ∈ 𝑌))
9592, 93, 94sylanbrc 694 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ (𝑌 × 𝑌))
96 simp-5r 804 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ))
9782, 96eqeltrrd 2688 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ))
9850simprbi 478 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ) → ¬ 𝑥 𝑦)
9997, 98syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 𝑦)
1006ad5antr 765 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
101100, 85, 86, 44syl3anc 1317 . . . . . . . . . . . . . . 15 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 𝑦 ↔ (𝐹𝑥) = (𝐹𝑦)))
102101necon3bbid 2818 . . . . . . . . . . . . . 14 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 𝑦 ↔ (𝐹𝑥) ≠ (𝐹𝑦)))
10399, 102mpbid 220 . . . . . . . . . . . . 13 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) ≠ (𝐹𝑦))
10495, 103, 39sylanbrc 694 . . . . . . . . . . . 12 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
10588, 104eqeltrd 2687 . . . . . . . . . . 11 ((((((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝑋) ∧ 𝑦𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
106 eldifi 3693 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑋 × 𝑋) ∖ ) → 𝑧 ∈ (𝑋 × 𝑋))
107106adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → 𝑧 ∈ (𝑋 × 𝑋))
108 elxp2 5046 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
109107, 108sylib 206 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
110109adantr 479 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝑋𝑦𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
111105, 110r19.29vva 3061 . . . . . . . . . 10 (((𝜑𝑧 ∈ ((𝑋 × 𝑋) ∖ )) ∧ (𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
112111r19.29an 3058 . . . . . . . . 9 ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
11381, 112impbida 872 . . . . . . . 8 (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
114 opex 4853 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
11552, 114fnmpt2i 7106 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑋)
116 difss 3698 . . . . . . . . 9 ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)
117 fvelimab 6148 . . . . . . . . 9 ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐))
118115, 116, 117mp2an 703 . . . . . . . 8 (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ )(𝐻𝑧) = 𝑐)
119113, 118syl6rbbr 277 . . . . . . 7 (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
120119eqrdv 2607 . . . . . 6 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ I ))
121 ssv 3587 . . . . . . 7 𝑌 ⊆ V
122 xpss2 5141 . . . . . . 7 (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
123 difres 28629 . . . . . . 7 ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
124121, 122, 123mp2b 10 . . . . . 6 ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
125120, 124syl6eqr 2661 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
1267toptopon 20496 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
1273, 126sylib 206 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
128 qtoptopon 21265 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129127, 4, 128syl2anc 690 . . . . . 6 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
130 qtophaus.3 . . . . . 6 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
131130ralrimiva 2948 . . . . . . . 8 (𝜑 → ∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹))
132 imaeq2 5368 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
133132eleq1d 2671 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹𝑦) ∈ (𝐽 qTop 𝐹)))
134133cbvralv 3146 . . . . . . . 8 (∀𝑥𝐽 (𝐹𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
135131, 134sylib 206 . . . . . . 7 (𝜑 → ∀𝑦𝐽 (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
136135r19.21bi 2915 . . . . . 6 ((𝜑𝑦𝐽) → (𝐹𝑦) ∈ (𝐽 qTop 𝐹))
1377, 7txuni 21153 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
1383, 3, 137syl2anc 690 . . . . . . . 8 (𝜑 → (𝑋 × 𝑋) = (𝐽 ×t 𝐽))
139138difeq1d 3688 . . . . . . 7 (𝜑 → ((𝑋 × 𝑋) ∖ ) = ( (𝐽 ×t 𝐽) ∖ ))
140 qtophaus.4 . . . . . . . 8 (𝜑 ∈ (Clsd‘(𝐽 ×t 𝐽)))
141 txtop 21130 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
1423, 3, 141syl2anc 690 . . . . . . . . 9 (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
143 fcoinver 28632 . . . . . . . . . . . . 13 (𝐹 Fn 𝑋 → (𝐹𝐹) Er 𝑋)
1446, 143syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐹) Er 𝑋)
145 ereq1 7614 . . . . . . . . . . . . 13 ( = (𝐹𝐹) → ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋))
14643, 145ax-mp 5 . . . . . . . . . . . 12 ( Er 𝑋 ↔ (𝐹𝐹) Er 𝑋)
147144, 146sylibr 222 . . . . . . . . . . 11 (𝜑 Er 𝑋)
148 erssxp 7630 . . . . . . . . . . 11 ( Er 𝑋 ⊆ (𝑋 × 𝑋))
149147, 148syl 17 . . . . . . . . . 10 (𝜑 ⊆ (𝑋 × 𝑋))
150149, 138sseqtrd 3603 . . . . . . . . 9 (𝜑 (𝐽 ×t 𝐽))
151 eqid 2609 . . . . . . . . . 10 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
152151iscld2 20590 . . . . . . . . 9 (((𝐽 ×t 𝐽) ∈ Top ∧ (𝐽 ×t 𝐽)) → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
153142, 150, 152syl2anc 690 . . . . . . . 8 (𝜑 → ( ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽)))
154140, 153mpbid 220 . . . . . . 7 (𝜑 → ( (𝐽 ×t 𝐽) ∖ ) ∈ (𝐽 ×t 𝐽))
155139, 154eqeltrd 2687 . . . . . 6 (𝜑 → ((𝑋 × 𝑋) ∖ ) ∈ (𝐽 ×t 𝐽))
15690, 90, 127, 127, 129, 129, 130, 136, 155, 52txomap 29063 . . . . 5 (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157125, 156eqeltrrd 2688 . . . 4 (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15823, 157eqeltrd 2687 . . 3 (𝜑 → ( ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
159 eqid 2609 . . . . 5 ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
160159iscld2 20590 . . . 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 500 . . 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 1316 . 2 (𝜑 → ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
16313hausdiag 21206 . 2 ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
1649, 162, 163sylanbrc 694 1 (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  cdif 3536  wss 3539  cop 4130   cuni 4366   class class class wbr 4577   I cid 4938   × cxp 5026  ccnv 5027  cres 5030  cima 5031  ccom 5032  Rel wrel 5033  Fun wfun 5784   Fn wfn 5785  wf 5786  ontowfo 5788  cfv 5790  (class class class)co 6527  cmpt2 6529   Er wer 7604   qTop cqtop 15935  Topctop 20465  TopOnctopon 20466  Clsdccld 20578  Hauscha 20870   ×t ctx 21121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7037  df-2nd 7038  df-er 7607  df-topgen 15876  df-qtop 15939  df-top 20469  df-bases 20470  df-topon 20471  df-cld 20581  df-haus 20877  df-tx 21123
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator