Theorem qtophaus 33996

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 23306	. . . 4 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
4		qtophaus.2	. . . 4 ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)
5		fofn 6748	. . . 4 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝑋)
7		qtophaus.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
8	7	qtoptop 23675	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
9	3, 6, 8	syl2anc 585	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10		txtop 23544	. . . 4 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
11	9, 9, 10	syl2anc 585	. . 3 ⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12		idssxp 6008	. . . 4 ⊢ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹))
13		eqid 2737	. . . . . 6 ⊢ ∪ (𝐽 qTop 𝐹) = ∪ (𝐽 qTop 𝐹)
14	13, 13	txuni 23567	. . . . 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 3965	. . 3 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
17	7	qtopuni 23677	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
18	3, 4, 17	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹))
19	18	sqxpeqd 5656	. . . . . 6 ⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)))
20	19, 15	eqtr2d 2773	. . . . 5 ⊢ (𝜑 → ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
21	18	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → ∪ (𝐽 qTop 𝐹) = 𝑌)
22	21	reseq2d 5938	. . . . 5 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
23	20, 22	difeq12d 4068	. . . 4 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24		qtophaus.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
25		opex 5411	. . . . . . . . . 10 ⊢ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ V
26	24, 25	fnmpoi 8016	. . . . . . . . 9 ⊢ 𝐻 Fn (𝑋 × 𝑋)
27		difss 4077	. . . . . . . . 9 ⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)
28		fvelimab 6906	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
29	26, 27, 28	mp2an 693	. . . . . . . 8 ⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
30		simp-4r 784	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋)
31		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋)
32		opelxpi 5661	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
33	30, 31, 32	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
34		df-br 5087	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
35	33, 34	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
36		simpllr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎)
37		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏)
38	36, 37	opeq12d 4825	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨𝑎, 𝑏⟩)
39		simp-5r 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
40		simp-8r 792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
41	39, 40	eqeltrrd 2838	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
42	38, 41	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
43		relxp 5642	. . . . . . . . . . . . . . . . . 18 ⊢ Rel (𝑌 × 𝑌)
44		opeldifid 32684	. . . . . . . . . . . . . . . . . 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 32690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
51	48, 30, 31, 50	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
52	51	necon3bbid 2970	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
53	47, 52	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦)
54		df-br 5087	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
55		brdif 5139	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
56	54, 55	bitr3i 277	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
57	35, 53, 56	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
58	24, 30, 31	fvproj 8077	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
59	38, 58, 39	3eqtr4d 2782	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
60		fveqeq2 6843	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
61	60	rspcev 3565	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
62	57, 59, 61	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
63		fofun 6747	. . . . . . . . . . . . . . . 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 6751	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌)
69	4, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌)
70	69	ad4antr 733	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹 “ 𝑋) = 𝑌)
71	70	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌)
72	67, 71	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋))
73		fvelima 6899	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
74	66, 72, 73	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
75	62, 74	r19.29a 3146	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
76		simpllr 776	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝑌)
77	76, 70	eleqtrrd 2840	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹 “ 𝑋))
78		fvelima 6899	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
79	65, 77, 78	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
80	75, 79	r19.29a 3146	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
82	81	eldifad 3902	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
83		elxp2 5648	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
84	82, 83	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
85	80, 84	r19.29vva 3198	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
86		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
87	86	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
88		simp-4r 784	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = 𝑐)
89		simpllr 776	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥 ∈ 𝑋)
90		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦 ∈ 𝑋)
91	24, 89, 90	fvproj 8077	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
92	87, 88, 91	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
93		fof 6746	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
94	4, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
95	94	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋⟶𝑌)
96	95, 89	ffvelcdmd 7031	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ∈ 𝑌)
97	95, 90	ffvelcdmd 7031	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑦) ∈ 𝑌)
98		opelxp 5660	. . . . . . . . . . . . . 14 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌))
99	96, 97, 98	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌))
100		simp-5r 786	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ))
101	86, 100	eqeltrrd 2838	. . . . . . . . . . . . . . 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 2970	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
107	103, 106	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
108	99, 107, 45	sylanbrc 584	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
109	92, 108	eqeltrd 2837	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
110		eldifi 4072	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋))
111	110	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋))
112		elxp2 5648	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
113	111, 112	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
114	113	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
115	109, 114	r19.29vva 3198	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
116	115	r19.29an 3142	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
117	85, 116	impbida 801	. . . . . . . 8 ⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
118	29, 117	bitr4id 290	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119	118	eqrdv 2735	. . . . . 6 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I ))
120		ssv 3947	. . . . . . 7 ⊢ 𝑌 ⊆ V
121		xpss2 5644	. . . . . . 7 ⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122		difres 32685	. . . . . . 7 ⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123	120, 121, 122	mp2b 10	. . . . . 6 ⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124	119, 123	eqtr4di 2790	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
125	7	toptopon 22892	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
126	3, 125	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
127		qtoptopon 23679	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128	126, 4, 127	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129		qtophaus.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
130	129	ralrimiva 3130	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
131		imaeq2 6015	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
132	131	eleq1d 2822	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)))
133	132	cbvralvw 3216	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
134	130, 133	sylib 218	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
135	134	r19.21bi 3230	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
136	7, 7	txuni 23567	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
137	3, 3, 136	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
138	137	difeq1d 4066	. . . . . . 7 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽 ×t 𝐽) ∖ ∼ ))
139		qtophaus.4	. . . . . . . 8 ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))
140		txtop 23544	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
141	3, 3, 140	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142		fcoinver 32689	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
143	6, 142	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋)
144		ereq1 8644	. . . . . . . . . . . . 13 ⊢ ( ∼ = (◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋))
145	49, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)
146	143, 145	sylibr 234	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ Er 𝑋)
147		erssxp 8660	. . . . . . . . . . 11 ⊢ ( ∼ Er 𝑋 → ∼ ⊆ (𝑋 × 𝑋))
148	146, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋))
149	148, 137	sseqtrd 3959	. . . . . . . . 9 ⊢ (𝜑 → ∼ ⊆ ∪ (𝐽 ×t 𝐽))
150		eqid 2737	. . . . . . . . . 10 ⊢ ∪ (𝐽 ×t 𝐽) = ∪ (𝐽 ×t 𝐽)
151	150	iscld2 23003	. . . . . . . . 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 2837	. . . . . 6 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
155	94, 94, 126, 126, 128, 128, 129, 135, 154, 24	txomap 33994	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156	124, 155	eqeltrrd 2838	. . . 4 ⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157	23, 156	eqeltrd 2837	. . 3 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158		eqid 2737	. . . . 5 ⊢ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159	158	iscld2 23003	. . . 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 23620	. 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 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890  ⟨cop 4574  ∪ cuni 4851   class class class wbr 5086   I cid 5518   × cxp 5622  ^◡ccnv 5623   ↾ cres 5626   “ cima 5627   ∘ ccom 5628  Rel wrel 5629  Fun wfun 6486   Fn wfn 6487  ⟶wf 6488  –onto→wfo 6490  ‘cfv 6492  (class class class)co 7360   ∈ cmpo 7362   Er wer 8633   qTop cqtop 17458  Topctop 22868  TopOnctopon 22885  Clsdccld 22991  Hauscha 23283   ×_t ctx 23535

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 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-er 8636  df-topgen 17397  df-qtop 17462  df-top 22869  df-topon 22886  df-bases 22921  df-cld 22994  df-haus 23290  df-tx 23537

This theorem is referenced by: (None)