Theorem qtophaus 33114

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 23055	. . . 4 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
4		qtophaus.2	. . . 4 ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)
5		fofn 6806	. . . 4 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝑋)
7		qtophaus.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
8	7	qtoptop 23424	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
9	3, 6, 8	syl2anc 582	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10		txtop 23293	. . . 4 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
11	9, 9, 10	syl2anc 582	. . 3 ⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12		idssxp 6047	. . . 4 ⊢ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹))
13		eqid 2730	. . . . . 6 ⊢ ∪ (𝐽 qTop 𝐹) = ∪ (𝐽 qTop 𝐹)
14	13, 13	txuni 23316	. . . . 5 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15	9, 9, 14	syl2anc 582	. . . 4 ⊢ (𝜑 → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
16	12, 15	sseqtrid 4033	. . 3 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
17	7	qtopuni 23426	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
18	3, 4, 17	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹))
19	18	sqxpeqd 5707	. . . . . 6 ⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)))
20	19, 15	eqtr2d 2771	. . . . 5 ⊢ (𝜑 → ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
21	18	eqcomd 2736	. . . . . 6 ⊢ (𝜑 → ∪ (𝐽 qTop 𝐹) = 𝑌)
22	21	reseq2d 5980	. . . . 5 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
23	20, 22	difeq12d 4122	. . . 4 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24		qtophaus.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
25		opex 5463	. . . . . . . . . 10 ⊢ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ V
26	24, 25	fnmpoi 8058	. . . . . . . . 9 ⊢ 𝐻 Fn (𝑋 × 𝑋)
27		difss 4130	. . . . . . . . 9 ⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)
28		fvelimab 6963	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
29	26, 27, 28	mp2an 688	. . . . . . . 8 ⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
30		simp-4r 780	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋)
31		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋)
32		opelxpi 5712	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
33	30, 31, 32	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
34		df-br 5148	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
35	33, 34	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
36		simpllr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎)
37		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏)
38	36, 37	opeq12d 4880	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨𝑎, 𝑏⟩)
39		simp-5r 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
40		simp-8r 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
41	39, 40	eqeltrrd 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
42	38, 41	eqeltrd 2831	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
43		relxp 5693	. . . . . . . . . . . . . . . . . 18 ⊢ Rel (𝑌 × 𝑌)
44		opeldifid 32097	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel (𝑌 × 𝑌) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))))
45	43, 44	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
46	42, 45	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
47	46	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
48	6	ad8antr 736	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋)
49		qtophaus.e	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ = (◡𝐹 ∘ 𝐹)
50	49	fcoinvbr 32103	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
51	48, 30, 31, 50	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
52	51	necon3bbid 2976	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
53	47, 52	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦)
54		df-br 5148	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
55		brdif 5200	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
56	54, 55	bitr3i 276	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
57	35, 53, 56	sylanbrc 581	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
58	24, 30, 31	fvproj 8122	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
59	38, 58, 39	3eqtr4d 2780	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
60		fveqeq2 6899	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
61	60	rspcev 3611	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
62	57, 59, 61	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
63		fofun 6805	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹)
64	4, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐹)
65	64	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
66	65	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹)
67		simp-4r 780	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌)
68		foima 6809	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌)
69	4, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌)
70	69	ad4antr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹 “ 𝑋) = 𝑌)
71	70	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌)
72	67, 71	eleqtrrd 2834	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋))
73		fvelima 6956	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
74	66, 72, 73	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
75	62, 74	r19.29a 3160	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
76		simpllr 772	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝑌)
77	76, 70	eleqtrrd 2834	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹 “ 𝑋))
78		fvelima 6956	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
79	65, 77, 78	syl2anc 582	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
80	75, 79	r19.29a 3160	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
81		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
82	81	eldifad 3959	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
83		elxp2 5699	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
84	82, 83	sylib 217	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
85	80, 84	r19.29vva 3211	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
86		simpr 483	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
87	86	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
88		simp-4r 780	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = 𝑐)
89		simpllr 772	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥 ∈ 𝑋)
90		simplr 765	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦 ∈ 𝑋)
91	24, 89, 90	fvproj 8122	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
92	87, 88, 91	3eqtr3d 2778	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
93		fof 6804	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
94	4, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
95	94	ad5antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋⟶𝑌)
96	95, 89	ffvelcdmd 7086	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ∈ 𝑌)
97	95, 90	ffvelcdmd 7086	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑦) ∈ 𝑌)
98		opelxp 5711	. . . . . . . . . . . . . 14 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌))
99	96, 97, 98	sylanbrc 581	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌))
100		simp-5r 782	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ))
101	86, 100	eqeltrrd 2832	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
102	56	simprbi 495	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬ 𝑥 ∼ 𝑦)
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 ∼ 𝑦)
104	6	ad5antr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
105	104, 89, 90, 50	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
106	105	necon3bbid 2976	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
107	103, 106	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
108	99, 107, 45	sylanbrc 581	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
109	92, 108	eqeltrd 2831	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
110		eldifi 4125	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋))
111	110	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋))
112		elxp2 5699	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
113	111, 112	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
114	113	adantr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
115	109, 114	r19.29vva 3211	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
116	115	r19.29an 3156	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
117	85, 116	impbida 797	. . . . . . . 8 ⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
118	29, 117	bitr4id 289	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119	118	eqrdv 2728	. . . . . 6 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I ))
120		ssv 4005	. . . . . . 7 ⊢ 𝑌 ⊆ V
121		xpss2 5695	. . . . . . 7 ⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122		difres 32098	. . . . . . 7 ⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123	120, 121, 122	mp2b 10	. . . . . 6 ⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124	119, 123	eqtr4di 2788	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
125	7	toptopon 22639	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
126	3, 125	sylib 217	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
127		qtoptopon 23428	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128	126, 4, 127	syl2anc 582	. . . . . 6 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129		qtophaus.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
130	129	ralrimiva 3144	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
131		imaeq2 6054	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
132	131	eleq1d 2816	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)))
133	132	cbvralvw 3232	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
134	130, 133	sylib 217	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
135	134	r19.21bi 3246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
136	7, 7	txuni 23316	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
137	3, 3, 136	syl2anc 582	. . . . . . . 8 ⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
138	137	difeq1d 4120	. . . . . . 7 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽 ×t 𝐽) ∖ ∼ ))
139		qtophaus.4	. . . . . . . 8 ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))
140		txtop 23293	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
141	3, 3, 140	syl2anc 582	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142		fcoinver 32102	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
143	6, 142	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋)
144		ereq1 8712	. . . . . . . . . . . . 13 ⊢ ( ∼ = (◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋))
145	49, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)
146	143, 145	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ Er 𝑋)
147		erssxp 8728	. . . . . . . . . . 11 ⊢ ( ∼ Er 𝑋 → ∼ ⊆ (𝑋 × 𝑋))
148	146, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋))
149	148, 137	sseqtrd 4021	. . . . . . . . 9 ⊢ (𝜑 → ∼ ⊆ ∪ (𝐽 ×t 𝐽))
150		eqid 2730	. . . . . . . . . 10 ⊢ ∪ (𝐽 ×t 𝐽) = ∪ (𝐽 ×t 𝐽)
151	150	iscld2 22752	. . . . . . . . 9 ⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼ ⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
152	141, 149, 151	syl2anc 582	. . . . . . . 8 ⊢ (𝜑 → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
153	139, 152	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
154	138, 153	eqeltrd 2831	. . . . . 6 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
155	94, 94, 126, 126, 128, 128, 129, 135, 154, 24	txomap 33112	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156	124, 155	eqeltrrd 2832	. . . 4 ⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157	23, 156	eqeltrd 2831	. . 3 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158		eqid 2730	. . . . 5 ⊢ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159	158	iscld2 22752	. . . 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 476	. . 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 834	. 2 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
162	13	hausdiag 23369	. 2 ⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
163	9, 161, 162	sylanbrc 581	1 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3472   ∖ cdif 3944   ⊆ wss 3947  ⟨cop 4633  ∪ cuni 4907   class class class wbr 5147   I cid 5572   × cxp 5673  ^◡ccnv 5674   ↾ cres 5677   “ cima 5678   ∘ ccom 5679  Rel wrel 5680  Fun wfun 6536   Fn wfn 6537  ⟶wf 6538  –onto→wfo 6540  ‘cfv 6542  (class class class)co 7411   ∈ cmpo 7413   Er wer 8702   qTop cqtop 17453  Topctop 22615  TopOnctopon 22632  Clsdccld 22740  Hauscha 23032   ×_t ctx 23284

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-er 8705  df-topgen 17393  df-qtop 17457  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-haus 23039  df-tx 23286

This theorem is referenced by: (None)