Theorem qtophaus 33782

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.

Step	Hyp	Ref	Expression
1		qtophaus.1	. . . 4 ⊢ (𝜑 → 𝐽 ∈ Haus)
2		haustop 23360	. . . 4 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
4		qtophaus.2	. . . 4 ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)
5		fofn 6836	. . . 4 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝑋)
7		qtophaus.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
8	7	qtoptop 23729	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
9	3, 6, 8	syl2anc 583	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10		txtop 23598	. . . 4 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
11	9, 9, 10	syl2anc 583	. . 3 ⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12		idssxp 6078	. . . 4 ⊢ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹))
13		eqid 2740	. . . . . 6 ⊢ ∪ (𝐽 qTop 𝐹) = ∪ (𝐽 qTop 𝐹)
14	13, 13	txuni 23621	. . . . 5 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15	9, 9, 14	syl2anc 583	. . . 4 ⊢ (𝜑 → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
16	12, 15	sseqtrid 4061	. . 3 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
17	7	qtopuni 23731	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
18	3, 4, 17	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹))
19	18	sqxpeqd 5732	. . . . . 6 ⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)))
20	19, 15	eqtr2d 2781	. . . . 5 ⊢ (𝜑 → ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
21	18	eqcomd 2746	. . . . . 6 ⊢ (𝜑 → ∪ (𝐽 qTop 𝐹) = 𝑌)
22	21	reseq2d 6009	. . . . 5 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
23	20, 22	difeq12d 4150	. . . 4 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24		qtophaus.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
25		opex 5484	. . . . . . . . . 10 ⊢ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ V
26	24, 25	fnmpoi 8111	. . . . . . . . 9 ⊢ 𝐻 Fn (𝑋 × 𝑋)
27		difss 4159	. . . . . . . . 9 ⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)
28		fvelimab 6994	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
29	26, 27, 28	mp2an 691	. . . . . . . 8 ⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
30		simp-4r 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋)
31		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋)
32		opelxpi 5737	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
33	30, 31, 32	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
34		df-br 5167	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
35	33, 34	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
36		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎)
37		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏)
38	36, 37	opeq12d 4905	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨𝑎, 𝑏⟩)
39		simp-5r 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
40		simp-8r 791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
41	39, 40	eqeltrrd 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
42	38, 41	eqeltrd 2844	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
43		relxp 5718	. . . . . . . . . . . . . . . . . 18 ⊢ Rel (𝑌 × 𝑌)
44		opeldifid 32621	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel (𝑌 × 𝑌) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))))
45	43, 44	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
46	42, 45	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
47	46	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
48	6	ad8antr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋)
49		qtophaus.e	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ = (◡𝐹 ∘ 𝐹)
50	49	fcoinvbr 32627	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
51	48, 30, 31, 50	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
52	51	necon3bbid 2984	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
53	47, 52	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦)
54		df-br 5167	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
55		brdif 5219	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
56	54, 55	bitr3i 277	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
57	35, 53, 56	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
58	24, 30, 31	fvproj 8175	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
59	38, 58, 39	3eqtr4d 2790	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
60		fveqeq2 6929	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
61	60	rspcev 3635	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
62	57, 59, 61	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
63		fofun 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹)
64	4, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐹)
65	64	ad4antr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
66	65	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹)
67		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌)
68		foima 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌)
69	4, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌)
70	69	ad4antr 731	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹 “ 𝑋) = 𝑌)
71	70	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌)
72	67, 71	eleqtrrd 2847	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋))
73		fvelima 6987	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
74	66, 72, 73	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
75	62, 74	r19.29a 3168	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
76		simpllr 775	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝑌)
77	76, 70	eleqtrrd 2847	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹 “ 𝑋))
78		fvelima 6987	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
79	65, 77, 78	syl2anc 583	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
80	75, 79	r19.29a 3168	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
82	81	eldifad 3988	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
83		elxp2 5724	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
84	82, 83	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
85	80, 84	r19.29vva 3222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
86		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
87	86	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
88		simp-4r 783	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = 𝑐)
89		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥 ∈ 𝑋)
90		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦 ∈ 𝑋)
91	24, 89, 90	fvproj 8175	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
92	87, 88, 91	3eqtr3d 2788	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
93		fof 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
94	4, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
95	94	ad5antr 733	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋⟶𝑌)
96	95, 89	ffvelcdmd 7119	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ∈ 𝑌)
97	95, 90	ffvelcdmd 7119	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑦) ∈ 𝑌)
98		opelxp 5736	. . . . . . . . . . . . . 14 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌))
99	96, 97, 98	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌))
100		simp-5r 785	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ))
101	86, 100	eqeltrrd 2845	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
102	56	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬ 𝑥 ∼ 𝑦)
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 ∼ 𝑦)
104	6	ad5antr 733	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
105	104, 89, 90, 50	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
106	105	necon3bbid 2984	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
107	103, 106	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
108	99, 107, 45	sylanbrc 582	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
109	92, 108	eqeltrd 2844	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
110		eldifi 4154	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋))
111	110	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋))
112		elxp2 5724	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
113	111, 112	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
114	113	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
115	109, 114	r19.29vva 3222	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
116	115	r19.29an 3164	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
117	85, 116	impbida 800	. . . . . . . 8 ⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
118	29, 117	bitr4id 290	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119	118	eqrdv 2738	. . . . . 6 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I ))
120		ssv 4033	. . . . . . 7 ⊢ 𝑌 ⊆ V
121		xpss2 5720	. . . . . . 7 ⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122		difres 32622	. . . . . . 7 ⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123	120, 121, 122	mp2b 10	. . . . . 6 ⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124	119, 123	eqtr4di 2798	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
125	7	toptopon 22944	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
126	3, 125	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
127		qtoptopon 23733	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128	126, 4, 127	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129		qtophaus.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
130	129	ralrimiva 3152	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
131		imaeq2 6085	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
132	131	eleq1d 2829	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)))
133	132	cbvralvw 3243	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
134	130, 133	sylib 218	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
135	134	r19.21bi 3257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
136	7, 7	txuni 23621	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
137	3, 3, 136	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
138	137	difeq1d 4148	. . . . . . 7 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽 ×t 𝐽) ∖ ∼ ))
139		qtophaus.4	. . . . . . . 8 ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))
140		txtop 23598	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
141	3, 3, 140	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142		fcoinver 32626	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
143	6, 142	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋)
144		ereq1 8770	. . . . . . . . . . . . 13 ⊢ ( ∼ = (◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋))
145	49, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)
146	143, 145	sylibr 234	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ Er 𝑋)
147		erssxp 8786	. . . . . . . . . . 11 ⊢ ( ∼ Er 𝑋 → ∼ ⊆ (𝑋 × 𝑋))
148	146, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋))
149	148, 137	sseqtrd 4049	. . . . . . . . 9 ⊢ (𝜑 → ∼ ⊆ ∪ (𝐽 ×t 𝐽))
150		eqid 2740	. . . . . . . . . 10 ⊢ ∪ (𝐽 ×t 𝐽) = ∪ (𝐽 ×t 𝐽)
151	150	iscld2 23057	. . . . . . . . 9 ⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼ ⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
152	141, 149, 151	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
153	139, 152	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
154	138, 153	eqeltrd 2844	. . . . . 6 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
155	94, 94, 126, 126, 128, 128, 129, 135, 154, 24	txomap 33780	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156	124, 155	eqeltrrd 2845	. . . 4 ⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157	23, 156	eqeltrd 2844	. . 3 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158		eqid 2740	. . . . 5 ⊢ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159	158	iscld2 23057	. . . 4 ⊢ ((((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) → (( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))) ↔ (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
160	159	biimpar 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 𝐹))))
161	11, 16, 157, 160	syl21anc 837	. 2 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
162	13	hausdiag 23674	. 2 ⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
163	9, 161, 162	sylanbrc 582	1 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973   ⊆ wss 3976  ⟨cop 4654  ∪ cuni 4931   class class class wbr 5166   I cid 5592   × cxp 5698  ^◡ccnv 5699   ↾ cres 5702   “ cima 5703   ∘ ccom 5704  Rel wrel 5705  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  –onto→wfo 6571  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450   Er wer 8760   qTop cqtop 17563  Topctop 22920  TopOnctopon 22937  Clsdccld 23045  Hauscha 23337   ×_t ctx 23589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-er 8763  df-topgen 17503  df-qtop 17567  df-top 22921  df-topon 22938  df-bases 22974  df-cld 23048  df-haus 23344  df-tx 23591

This theorem is referenced by: (None)