Theorem qtophaus 31100

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 21939	. . . 4 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝐽 ∈ Top)
4		qtophaus.2	. . . 4 ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)
5		fofn 6592	. . . 4 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋)
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝑋)
7		qtophaus.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
8	7	qtoptop 22308	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top)
9	3, 6, 8	syl2anc 586	. 2 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
10		txtop 22177	. . . 4 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
11	9, 9, 10	syl2anc 586	. . 3 ⊢ (𝜑 → ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∈ Top)
12		idssxp 5916	. . . 4 ⊢ ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹))
13		eqid 2821	. . . . . 6 ⊢ ∪ (𝐽 qTop 𝐹) = ∪ (𝐽 qTop 𝐹)
14	13, 13	txuni 22200	. . . . 5 ⊢ (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
15	9, 9, 14	syl2anc 586	. . . 4 ⊢ (𝜑 → (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
16	12, 15	sseqtrid 4019	. . 3 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ⊆ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
17	7	qtopuni 22310	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹))
18	3, 4, 17	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ∪ (𝐽 qTop 𝐹))
19	18	sqxpeqd 5587	. . . . . 6 ⊢ (𝜑 → (𝑌 × 𝑌) = (∪ (𝐽 qTop 𝐹) × ∪ (𝐽 qTop 𝐹)))
20	19, 15	eqtr2d 2857	. . . . 5 ⊢ (𝜑 → ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = (𝑌 × 𝑌))
21	18	eqcomd 2827	. . . . . 6 ⊢ (𝜑 → ∪ (𝐽 qTop 𝐹) = 𝑌)
22	21	reseq2d 5853	. . . . 5 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) = ( I ↾ 𝑌))
23	20, 22	difeq12d 4100	. . . 4 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
24		simp-4r 782	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥 ∈ 𝑋)
25		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑦 ∈ 𝑋)
26		opelxpi 5592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
27	24, 25, 26	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
28		df-br 5067	. . . . . . . . . . . . . . 15 ⊢ (𝑥(𝑋 × 𝑋)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑋))
29	27, 28	sylibr 236	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑥(𝑋 × 𝑋)𝑦)
30		simpllr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) = 𝑎)
31		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑦) = 𝑏)
32	30, 31	opeq12d 4811	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨𝑎, 𝑏⟩)
33		simp-5r 784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 = ⟨𝑎, 𝑏⟩)
34		simp-8r 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
35	33, 34	eqeltrrd 2914	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑎, 𝑏⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
36	32, 35	eqeltrd 2913	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
37		relxp 5573	. . . . . . . . . . . . . . . . . 18 ⊢ Rel (𝑌 × 𝑌)
38		opeldifid 30349	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel (𝑌 × 𝑌) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦))))
39	37, 38	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ) ↔ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
40	36, 39	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ∧ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
41	40	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
42	6	ad8antr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → 𝐹 Fn 𝑋)
43		qtophaus.e	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ = (◡𝐹 ∘ 𝐹)
44	43	fcoinvbr 30358	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
45	42, 24, 25, 44	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
46	45	necon3bbid 3053	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
47	41, 46	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ¬ 𝑥 ∼ 𝑦)
48		df-br 5067	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
49		brdif 5119	. . . . . . . . . . . . . . 15 ⊢ (𝑥((𝑋 × 𝑋) ∖ ∼ )𝑦 ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
50	48, 49	bitr3i 279	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ↔ (𝑥(𝑋 × 𝑋)𝑦 ∧ ¬ 𝑥 ∼ 𝑦))
51	29, 47, 50	sylanbrc 585	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
52		qtophaus.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
53	52, 24, 25	fvproj 7828	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
54	32, 53, 33	3eqtr4d 2866	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐)
55		fveqeq2 6679	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐))
56	55	rspcev 3623	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) ∧ (𝐻‘⟨𝑥, 𝑦⟩) = 𝑐) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
57	51, 54, 56	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑦) = 𝑏) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
58		fofun 6591	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹)
59	4, 58	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐹)
60	59	ad4antr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → Fun 𝐹)
61	60	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → Fun 𝐹)
62		simp-4r 782	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ 𝑌)
63		foima 6595	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌)
64	4, 63	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑋) = 𝑌)
65	64	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → (𝐹 “ 𝑋) = 𝑌)
66	65	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → (𝐹 “ 𝑋) = 𝑌)
67	62, 66	eleqtrrd 2916	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → 𝑏 ∈ (𝐹 “ 𝑋))
68		fvelima 6731	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 “ 𝑋)) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
69	61, 67, 68	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = 𝑏)
70	57, 69	r19.29a 3289	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) ∧ 𝑥 ∈ 𝑋) ∧ (𝐹‘𝑥) = 𝑎) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
71		simpllr 774	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ 𝑌)
72	71, 65	eleqtrrd 2916	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → 𝑎 ∈ (𝐹 “ 𝑋))
73		fvelima 6731	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑎 ∈ (𝐹 “ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
74	60, 72, 73	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑎)
75	70, 74	r19.29a 3289	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) ∧ 𝑎 ∈ 𝑌) ∧ 𝑏 ∈ 𝑌) ∧ 𝑐 = ⟨𝑎, 𝑏⟩) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
76		simpr 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
77	76	eldifad 3948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → 𝑐 ∈ (𝑌 × 𝑌))
78		elxp2 5579	. . . . . . . . . . 11 ⊢ (𝑐 ∈ (𝑌 × 𝑌) ↔ ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
79	77, 78	sylib 220	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑎 ∈ 𝑌 ∃𝑏 ∈ 𝑌 𝑐 = ⟨𝑎, 𝑏⟩)
80	75, 79	r19.29vva 3336	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )) → ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
81		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 = ⟨𝑥, 𝑦⟩)
82	81	fveq2d 6674	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
83		simp-4r 782	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘𝑧) = 𝑐)
84		simpllr 774	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑥 ∈ 𝑋)
85		simplr 767	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑦 ∈ 𝑋)
86	52, 84, 85	fvproj 7828	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐻‘⟨𝑥, 𝑦⟩) = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
87	82, 83, 86	3eqtr3d 2864	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
88		fof 6590	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
89	4, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
90	89	ad5antr 732	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹:𝑋⟶𝑌)
91	90, 84	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ∈ 𝑌)
92	90, 85	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑦) ∈ 𝑌)
93		opelxp 5591	. . . . . . . . . . . . . 14 ⊢ (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌) ↔ ((𝐹‘𝑥) ∈ 𝑌 ∧ (𝐹‘𝑦) ∈ 𝑌))
94	91, 92, 93	sylanbrc 585	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ (𝑌 × 𝑌))
95		simp-5r 784	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ))
96	81, 95	eqeltrrd 2914	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ))
97	50	simprbi 499	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝑋 × 𝑋) ∖ ∼ ) → ¬ 𝑥 ∼ 𝑦)
98	96, 97	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ¬ 𝑥 ∼ 𝑦)
99	6	ad5antr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝐹 Fn 𝑋)
100	99, 84, 85, 44	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
101	100	necon3bbid 3053	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (¬ 𝑥 ∼ 𝑦 ↔ (𝐹‘𝑥) ≠ (𝐹‘𝑦)))
102	98, 101	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
103	94, 102, 39	sylanbrc 585	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ ((𝑌 × 𝑌) ∖ I ))
104	87, 103	eqeltrd 2913	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨𝑥, 𝑦⟩) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
105		eldifi 4103	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ ) → 𝑧 ∈ (𝑋 × 𝑋))
106	105	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → 𝑧 ∈ (𝑋 × 𝑋))
107		elxp2 5579	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑋 × 𝑋) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
108	106, 107	sylib 220	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
109	108	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 𝑧 = ⟨𝑥, 𝑦⟩)
110	104, 109	r19.29vva 3336	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
111	110	r19.29an 3288	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝑌 × 𝑌) ∖ I ))
112	80, 111	impbida 799	. . . . . . . 8 ⊢ (𝜑 → (𝑐 ∈ ((𝑌 × 𝑌) ∖ I ) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
113		opex 5356	. . . . . . . . . 10 ⊢ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ ∈ V
114	52, 113	fnmpoi 7768	. . . . . . . . 9 ⊢ 𝐻 Fn (𝑋 × 𝑋)
115		difss 4108	. . . . . . . . 9 ⊢ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)
116		fvelimab 6737	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 × 𝑋) ∖ ∼ ) ⊆ (𝑋 × 𝑋)) → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐))
117	114, 115, 116	mp2an 690	. . . . . . . 8 ⊢ (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ ∃𝑧 ∈ ((𝑋 × 𝑋) ∖ ∼ )(𝐻‘𝑧) = 𝑐)
118	112, 117	syl6rbbr 292	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ↔ 𝑐 ∈ ((𝑌 × 𝑌) ∖ I )))
119	118	eqrdv 2819	. . . . . 6 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ I ))
120		ssv 3991	. . . . . . 7 ⊢ 𝑌 ⊆ V
121		xpss2 5575	. . . . . . 7 ⊢ (𝑌 ⊆ V → (𝑌 × 𝑌) ⊆ (𝑌 × V))
122		difres 30350	. . . . . . 7 ⊢ ((𝑌 × 𝑌) ⊆ (𝑌 × V) → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I ))
123	120, 121, 122	mp2b 10	. . . . . 6 ⊢ ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) = ((𝑌 × 𝑌) ∖ I )
124	119, 123	syl6eqr 2874	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) = ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)))
125	7	toptopon 21525	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
126	3, 125	sylib 220	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
127		qtoptopon 22312	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
128	126, 4, 127	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
129		qtophaus.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
130	129	ralrimiva 3182	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))
131		imaeq2 5925	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦))
132	131	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹)))
133	132	cbvralvw 3449	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
134	130, 133	sylib 220	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
135	134	r19.21bi 3208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝐹 “ 𝑦) ∈ (𝐽 qTop 𝐹))
136	7, 7	txuni 22200	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
137	3, 3, 136	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽))
138	137	difeq1d 4098	. . . . . . 7 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) = (∪ (𝐽 ×t 𝐽) ∖ ∼ ))
139		qtophaus.4	. . . . . . . 8 ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))
140		txtop 22177	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top)
141	3, 3, 140	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ×t 𝐽) ∈ Top)
142		fcoinver 30357	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋)
143	6, 142	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝐹 ∘ 𝐹) Er 𝑋)
144		ereq1 8296	. . . . . . . . . . . . 13 ⊢ ( ∼ = (◡𝐹 ∘ 𝐹) → ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋))
145	43, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ ( ∼ Er 𝑋 ↔ (◡𝐹 ∘ 𝐹) Er 𝑋)
146	143, 145	sylibr 236	. . . . . . . . . . 11 ⊢ (𝜑 → ∼ Er 𝑋)
147		erssxp 8312	. . . . . . . . . . 11 ⊢ ( ∼ Er 𝑋 → ∼ ⊆ (𝑋 × 𝑋))
148	146, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∼ ⊆ (𝑋 × 𝑋))
149	148, 137	sseqtrd 4007	. . . . . . . . 9 ⊢ (𝜑 → ∼ ⊆ ∪ (𝐽 ×t 𝐽))
150		eqid 2821	. . . . . . . . . 10 ⊢ ∪ (𝐽 ×t 𝐽) = ∪ (𝐽 ×t 𝐽)
151	150	iscld2 21636	. . . . . . . . 9 ⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ ∼ ⊆ ∪ (𝐽 ×t 𝐽)) → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
152	141, 149, 151	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → ( ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)) ↔ (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽)))
153	139, 152	mpbid 234	. . . . . . 7 ⊢ (𝜑 → (∪ (𝐽 ×t 𝐽) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
154	138, 153	eqeltrd 2913	. . . . . 6 ⊢ (𝜑 → ((𝑋 × 𝑋) ∖ ∼ ) ∈ (𝐽 ×t 𝐽))
155	89, 89, 126, 126, 128, 128, 129, 135, 154, 52	txomap 31098	. . . . 5 ⊢ (𝜑 → (𝐻 “ ((𝑋 × 𝑋) ∖ ∼ )) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
156	124, 155	eqeltrrd 2914	. . . 4 ⊢ (𝜑 → ((𝑌 × 𝑌) ∖ ( I ↾ 𝑌)) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
157	23, 156	eqeltrd 2913	. . 3 ⊢ (𝜑 → (∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) ∖ ( I ↾ ∪ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))
158		eqid 2821	. . . . 5 ⊢ ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)) = ∪ ((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))
159	158	iscld2 21636	. . . 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 480	. . 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 835	. 2 ⊢ (𝜑 → ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹))))
162	13	hausdiag 22253	. 2 ⊢ ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I ↾ ∪ (𝐽 qTop 𝐹)) ∈ (Clsd‘((𝐽 qTop 𝐹) ×t (𝐽 qTop 𝐹)))))
163	9, 161, 162	sylanbrc 585	1 ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ∖ cdif 3933   ⊆ wss 3936  ⟨cop 4573  ∪ cuni 4838   class class class wbr 5066   I cid 5459   × cxp 5553  ^◡ccnv 5554   ↾ cres 5557   “ cima 5558   ∘ ccom 5559  Rel wrel 5560  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351  –onto→wfo 6353  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158   Er wer 8286   qTop cqtop 16776  Topctop 21501  TopOnctopon 21518  Clsdccld 21624  Hauscha 21916   ×_t ctx 22168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-er 8289  df-topgen 16717  df-qtop 16780  df-top 21502  df-topon 21519  df-bases 21554  df-cld 21627  df-haus 21923  df-tx 22170

This theorem is referenced by: (None)