Theorem qtophaus 33980

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 23296	. . . 4 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
4		qtophaus.2	. . . 4 ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)
5		fofn 6754	. . . 4 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝑋)
7		qtophaus.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
8	7	qtoptop 23665	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
9	3, 6, 8	syl2anc 585	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10		txtop 23534	. . . 4 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
11	9, 9, 10	syl2anc 585	. . 3 ⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12		idssxp 6014	. . . 4 ⊢ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹))
13		eqid 2736	. . . . . 6 ⊢ ∪ (𝐽 qTop 𝐹) = ∪ (𝐽 qTop 𝐹)
14	13, 13	txuni 23557	. . . . 5 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15	9, 9, 14	syl2anc 585	. . . 4 ⊢ (𝜑 → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
16	12, 15	sseqtrid 3964	. . 3 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
17	7	qtopuni 23667	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
18	3, 4, 17	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹))
19	18	sqxpeqd 5663	. . . . . 6 ⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)))
20	19, 15	eqtr2d 2772	. . . . 5 ⊢ (𝜑 → ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
21	18	eqcomd 2742	. . . . . 6 ⊢ (𝜑 → ∪ (𝐽 qTop 𝐹) = 𝑌)
22	21	reseq2d 5944	. . . . 5 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
23	20, 22	difeq12d 4067	. . . 4 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24		qtophaus.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
25		opex 5416	. . . . . . . . . 10 ⊢ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ V
26	24, 25	fnmpoi 8023	. . . . . . . . 9 ⊢ 𝐻 Fn (𝑋 × 𝑋)
27		difss 4076	. . . . . . . . 9 ⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)
28		fvelimab 6912	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
29	26, 27, 28	mp2an 693	. . . . . . . 8 ⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
30		simp-4r 784	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋)
31		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋)
32		opelxpi 5668	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
33	30, 31, 32	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
34		df-br 5086	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
35	33, 34	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
36		simpllr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎)
37		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏)
38	36, 37	opeq12d 4824	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨𝑎, 𝑏⟩)
39		simp-5r 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
40		simp-8r 792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
41	39, 40	eqeltrrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
42	38, 41	eqeltrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
43		relxp 5649	. . . . . . . . . . . . . . . . . 18 ⊢ Rel (𝑌 × 𝑌)
44		opeldifid 32669	. . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋)
49		qtophaus.e	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ = (◡𝐹 ∘ 𝐹)
50	49	fcoinvbr 32675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
51	48, 30, 31, 50	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
52	51	necon3bbid 2969	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
53	47, 52	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦)
54		df-br 5086	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
55		brdif 5138	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
56	54, 55	bitr3i 277	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
57	35, 53, 56	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
58	24, 30, 31	fvproj 8084	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
59	38, 58, 39	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
60		fveqeq2 6849	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
61	60	rspcev 3564	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
62	57, 59, 61	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
63		fofun 6753	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹)
64	4, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐹)
65	64	ad4antr 733	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
66	65	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹)
67		simp-4r 784	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌)
68		foima 6757	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌)
69	4, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌)
70	69	ad4antr 733	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹 “ 𝑋) = 𝑌)
71	70	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌)
72	67, 71	eleqtrrd 2839	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋))
73		fvelima 6905	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
74	66, 72, 73	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
75	62, 74	r19.29a 3145	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
76		simpllr 776	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝑌)
77	76, 70	eleqtrrd 2839	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹 “ 𝑋))
78		fvelima 6905	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
79	65, 77, 78	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
80	75, 79	r19.29a 3145	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
82	81	eldifad 3901	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
83		elxp2 5655	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
84	82, 83	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
85	80, 84	r19.29vva 3197	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
86		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
87	86	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
88		simp-4r 784	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = 𝑐)
89		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥 ∈ 𝑋)
90		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦 ∈ 𝑋)
91	24, 89, 90	fvproj 8084	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
92	87, 88, 91	3eqtr3d 2779	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
93		fof 6752	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
94	4, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
95	94	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋⟶𝑌)
96	95, 89	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ∈ 𝑌)
97	95, 90	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑦) ∈ 𝑌)
98		opelxp 5667	. . . . . . . . . . . . . 14 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌))
99	96, 97, 98	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌))
100		simp-5r 786	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ))
101	86, 100	eqeltrrd 2837	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
102	56	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬ 𝑥 ∼ 𝑦)
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 ∼ 𝑦)
104	6	ad5antr 735	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
105	104, 89, 90, 50	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
106	105	necon3bbid 2969	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
107	103, 106	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
108	99, 107, 45	sylanbrc 584	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
109	92, 108	eqeltrd 2836	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
110		eldifi 4071	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋))
111	110	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋))
112		elxp2 5655	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
113	111, 112	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
114	113	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
115	109, 114	r19.29vva 3197	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
116	115	r19.29an 3141	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
117	85, 116	impbida 801	. . . . . . . 8 ⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
118	29, 117	bitr4id 290	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119	118	eqrdv 2734	. . . . . 6 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I ))
120		ssv 3946	. . . . . . 7 ⊢ 𝑌 ⊆ V
121		xpss2 5651	. . . . . . 7 ⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122		difres 32670	. . . . . . 7 ⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123	120, 121, 122	mp2b 10	. . . . . 6 ⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124	119, 123	eqtr4di 2789	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
125	7	toptopon 22882	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
126	3, 125	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
127		qtoptopon 23669	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128	126, 4, 127	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129		qtophaus.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
130	129	ralrimiva 3129	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
131		imaeq2 6021	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
132	131	eleq1d 2821	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)))
133	132	cbvralvw 3215	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
134	130, 133	sylib 218	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
135	134	r19.21bi 3229	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
136	7, 7	txuni 23557	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
137	3, 3, 136	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
138	137	difeq1d 4065	. . . . . . 7 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽 ×t 𝐽) ∖ ∼ ))
139		qtophaus.4	. . . . . . . 8 ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))
140		txtop 23534	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
141	3, 3, 140	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142		fcoinver 32674	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
143	6, 142	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋)
144		ereq1 8651	. . . . . . . . . . . . 13 ⊢ ( ∼ = (◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋))
145	49, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)
146	143, 145	sylibr 234	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ Er 𝑋)
147		erssxp 8667	. . . . . . . . . . 11 ⊢ ( ∼ Er 𝑋 → ∼ ⊆ (𝑋 × 𝑋))
148	146, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋))
149	148, 137	sseqtrd 3958	. . . . . . . . 9 ⊢ (𝜑 → ∼ ⊆ ∪ (𝐽 ×t 𝐽))
150		eqid 2736	. . . . . . . . . 10 ⊢ ∪ (𝐽 ×t 𝐽) = ∪ (𝐽 ×t 𝐽)
151	150	iscld2 22993	. . . . . . . . 9 ⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼ ⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
152	141, 149, 151	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
153	139, 152	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
154	138, 153	eqeltrd 2836	. . . . . 6 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
155	94, 94, 126, 126, 128, 128, 129, 135, 154, 24	txomap 33978	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156	124, 155	eqeltrrd 2837	. . . 4 ⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157	23, 156	eqeltrd 2836	. . 3 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158		eqid 2736	. . . . 5 ⊢ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159	158	iscld2 22993	. . . 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 838	. 2 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
162	13	hausdiag 23610	. 2 ⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
163	9, 161, 162	sylanbrc 584	1 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  Vcvv 3429   ∖ cdif 3886   ⊆ wss 3889  ⟨cop 4573  ∪ cuni 4850   class class class wbr 5085   I cid 5525   × cxp 5629  ^◡ccnv 5630   ↾ cres 5633   “ cima 5634   ∘ ccom 5635  Rel wrel 5636  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  –onto→wfo 6496  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369   Er wer 8640   qTop cqtop 17467  Topctop 22858  TopOnctopon 22875  Clsdccld 22981  Hauscha 23273   ×_t ctx 23525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-er 8643  df-topgen 17406  df-qtop 17471  df-top 22859  df-topon 22876  df-bases 22911  df-cld 22984  df-haus 23280  df-tx 23527

This theorem is referenced by: (None)