Metamath Proof Explorer

Theorem qtophaus

Description: If an open map's graph in the product space ( J tX J ) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020)

Ref Expression
Hypotheses qtophaus.x ⊢ 𝑋 = ∪ 𝐽
qtophaus.e ⊢ ∼ = ( ◡ 𝐹 ∘ 𝐹 )
qtophaus.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
qtophaus.1 ⊢ ( 𝜑 → 𝐽 ∈ Haus )
qtophaus.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
qtophaus.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
qtophaus.4 ⊢ ( 𝜑 → ∼ ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
Assertion qtophaus ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 qtophaus.x ⊢ 𝑋 = ∪ 𝐽
2 qtophaus.e ⊢ ∼ = ( ◡ 𝐹 ∘ 𝐹 )
3 qtophaus.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
4 qtophaus.1 ⊢ ( 𝜑 → 𝐽 ∈ Haus )
5 qtophaus.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
6 qtophaus.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
7 qtophaus.4 ⊢ ( 𝜑 → ∼ ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
8 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
9 4 8 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
10 fofn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 Fn 𝑋 )
11 5 10 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
12 1 qtoptop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 Fn 𝑋 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
13 9 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Top )
14 txtop ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ ( 𝐽 qTop 𝐹 ) ∈ Top ) → ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∈ Top )
15 13 13 14 syl2anc ⊢ ( 𝜑 → ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∈ Top )
16 idssxp ⊢ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ⊆ ( ∪ ( 𝐽 qTop 𝐹 ) × ∪ ( 𝐽 qTop 𝐹 ) )
17 eqid ⊢ ∪ ( 𝐽 qTop 𝐹 ) = ∪ ( 𝐽 qTop 𝐹 )
18 17 17 txuni ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ ( 𝐽 qTop 𝐹 ) ∈ Top ) → ( ∪ ( 𝐽 qTop 𝐹 ) × ∪ ( 𝐽 qTop 𝐹 ) ) = ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
19 13 13 18 syl2anc ⊢ ( 𝜑 → ( ∪ ( 𝐽 qTop 𝐹 ) × ∪ ( 𝐽 qTop 𝐹 ) ) = ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
20 16 19 sseqtrid ⊢ ( 𝜑 → ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
21 1 qtopuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
22 9 5 21 syl2anc ⊢ ( 𝜑 → 𝑌 = ∪ ( 𝐽 qTop 𝐹 ) )
23 22 sqxpeqd ⊢ ( 𝜑 → ( 𝑌 × 𝑌 ) = ( ∪ ( 𝐽 qTop 𝐹 ) × ∪ ( 𝐽 qTop 𝐹 ) ) )
24 23 19 eqtr2d ⊢ ( 𝜑 → ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) = ( 𝑌 × 𝑌 ) )
25 22 eqcomd ⊢ ( 𝜑 → ∪ ( 𝐽 qTop 𝐹 ) = 𝑌 )
26 25 reseq2d ⊢ ( 𝜑 → ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) = ( I ↾ 𝑌 ) )
27 24 26 difeq12d ⊢ ( 𝜑 → ( ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∖ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ) = ( ( 𝑌 × 𝑌 ) ∖ ( I ↾ 𝑌 ) ) )
28 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ V
29 3 28 fnmpoi ⊢ 𝐻 Fn ( 𝑋 × 𝑋 )
30 difss ⊢ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ⊆ ( 𝑋 × 𝑋 )
31 fvelimab ⊢ ( ( 𝐻 Fn ( 𝑋 × 𝑋 ) ∧ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑐 ∈ ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ↔ ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) )
32 29 30 31 mp2an ⊢ ( 𝑐 ∈ ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ↔ ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
33 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝑥 ∈ 𝑋 )
34 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝑦 ∈ 𝑋 )
35 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) )
36 33 34 35 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) )
37 df-br ⊢ ( 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) )
38 36 37 sylibr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝑥 ( 𝑋 × 𝑋 ) 𝑦 )
39 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝐹 ‘ 𝑥 ) = 𝑎 )
40 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝐹 ‘ 𝑦 ) = 𝑏 )
41 39 40 opeq12d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
42 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ )
43 simp-8r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
44 42 43 eqeltrrd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
45 41 44 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
46 relxp ⊢ Rel ( 𝑌 × 𝑌 )
47 opeldifid ⊢ ( Rel ( 𝑌 × 𝑌 ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ↔ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( 𝑌 × 𝑌 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) )
48 46 47 ax-mp ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ↔ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( 𝑌 × 𝑌 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
49 45 48 sylib ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( 𝑌 × 𝑌 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
50 49 simprd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
51 11 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → 𝐹 Fn 𝑋 )
52 2 fcoinvbr ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
53 51 33 34 52 syl3anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
54 53 necon3bbid ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( ¬ 𝑥 ∼ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
55 50 54 mpbird ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ¬ 𝑥 ∼ 𝑦 )
56 df-br ⊢ ( 𝑥 ( ( 𝑋 × 𝑋 ) ∖ ∼ ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) )
57 brdif ⊢ ( 𝑥 ( ( 𝑋 × 𝑋 ) ∖ ∼ ) 𝑦 ↔ ( 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ∧ ¬ 𝑥 ∼ 𝑦 ) )
58 56 57 bitr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ↔ ( 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ∧ ¬ 𝑥 ∼ 𝑦 ) )
59 38 55 58 sylanbrc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) )
60 3 33 34 fvproj ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
61 41 60 42 3eqtr4d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑐 )
62 fveqeq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐻 ‘ 𝑧 ) = 𝑐 ↔ ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑐 ) )
63 62 rspcev ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ∧ ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑐 ) → ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
64 59 61 63 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑏 ) → ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
65 fofun ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → Fun 𝐹 )
66 5 65 syl ⊢ ( 𝜑 → Fun 𝐹 )
67 66 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → Fun 𝐹 )
68 67 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → Fun 𝐹 )
69 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → 𝑏 ∈ 𝑌 )
70 foima ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( 𝐹 “ 𝑋 ) = 𝑌 )
71 5 70 syl ⊢ ( 𝜑 → ( 𝐹 “ 𝑋 ) = 𝑌 )
72 71 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
73 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
74 69 73 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → 𝑏 ∈ ( 𝐹 “ 𝑋 ) )
75 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑏 ∈ ( 𝐹 “ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = 𝑏 )
76 68 74 75 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → ∃ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) = 𝑏 )
77 64 76 r19.29a ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑎 ) → ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
78 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑎 ∈ 𝑌 )
79 78 72 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑎 ∈ ( 𝐹 “ 𝑋 ) )
80 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑎 ∈ ( 𝐹 “ 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑎 )
81 67 79 80 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑎 )
82 77 81 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) ∧ 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
83 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) → 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
84 83 eldifad ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) → 𝑐 ∈ ( 𝑌 × 𝑌 ) )
85 elxp2 ⊢ ( 𝑐 ∈ ( 𝑌 × 𝑌 ) ↔ ∃ 𝑎 ∈ 𝑌 ∃ 𝑏 ∈ 𝑌 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ )
86 84 85 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) → ∃ 𝑎 ∈ 𝑌 ∃ 𝑏 ∈ 𝑌 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ )
87 82 86 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) → ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
88 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
89 88 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
90 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = 𝑐 )
91 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 ∈ 𝑋 )
92 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ 𝑋 )
93 3 91 92 fvproj ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
94 89 90 93 3eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑐 = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
95 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
96 5 95 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
97 96 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐹 : 𝑋 ⟶ 𝑌 )
98 97 91 ffvelrnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
99 97 92 ffvelrnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
100 opelxp ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( 𝑌 × 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ) )
101 98 99 100 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( 𝑌 × 𝑌 ) )
102 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) )
103 88 102 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) )
104 58 simprbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) → ¬ 𝑥 ∼ 𝑦 )
105 103 104 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ¬ 𝑥 ∼ 𝑦 )
106 11 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐹 Fn 𝑋 )
107 106 91 92 52 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
108 107 necon3bbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ¬ 𝑥 ∼ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
109 105 108 mpbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
110 101 109 48 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
111 94 110 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
112 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) → 𝑧 ∈ ( 𝑋 × 𝑋 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) → 𝑧 ∈ ( 𝑋 × 𝑋 ) )
114 elxp2 ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
115 113 114 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
117 111 116 r19.29vva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
118 117 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) )
119 87 118 impbida ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ↔ ∃ 𝑧 ∈ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) )
120 32 119 bitr4id ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ↔ 𝑐 ∈ ( ( 𝑌 × 𝑌 ) ∖ I ) ) )
121 120 eqrdv ⊢ ( 𝜑 → ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) = ( ( 𝑌 × 𝑌 ) ∖ I ) )
122 ssv ⊢ 𝑌 ⊆ V
123 xpss2 ⊢ ( 𝑌 ⊆ V → ( 𝑌 × 𝑌 ) ⊆ ( 𝑌 × V ) )
124 difres ⊢ ( ( 𝑌 × 𝑌 ) ⊆ ( 𝑌 × V ) → ( ( 𝑌 × 𝑌 ) ∖ ( I ↾ 𝑌 ) ) = ( ( 𝑌 × 𝑌 ) ∖ I ) )
125 122 123 124 mp2b ⊢ ( ( 𝑌 × 𝑌 ) ∖ ( I ↾ 𝑌 ) ) = ( ( 𝑌 × 𝑌 ) ∖ I )
126 121 125 eqtr4di ⊢ ( 𝜑 → ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) = ( ( 𝑌 × 𝑌 ) ∖ ( I ↾ 𝑌 ) ) )
127 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
128 9 127 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
129 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
130 128 5 129 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
131 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
132 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
133 132 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝐹 “ 𝑦 ) ∈ ( 𝐽 qTop 𝐹 ) ) )
134 133 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝐹 “ 𝑦 ) ∈ ( 𝐽 qTop 𝐹 ) )
135 131 134 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐽 ( 𝐹 “ 𝑦 ) ∈ ( 𝐽 qTop 𝐹 ) )
136 135 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝐹 “ 𝑦 ) ∈ ( 𝐽 qTop 𝐹 ) )
137 1 1 txuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×t 𝐽 ) )
138 9 9 137 syl2anc ⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×t 𝐽 ) )
139 138 difeq1d ⊢ ( 𝜑 → ( ( 𝑋 × 𝑋 ) ∖ ∼ ) = ( ∪ ( 𝐽 ×t 𝐽 ) ∖ ∼ ) )
140 txtop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
141 9 9 140 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐽 ) ∈ Top )
142 fcoinver ⊢ ( 𝐹 Fn 𝑋 → ( ◡ 𝐹 ∘ 𝐹 ) Er 𝑋 )
143 11 142 syl ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) Er 𝑋 )
144 ereq1 ⊢ ( ∼ = ( ◡ 𝐹 ∘ 𝐹 ) → ( ∼ Er 𝑋 ↔ ( ◡ 𝐹 ∘ 𝐹 ) Er 𝑋 ) )
145 2 144 ax-mp ⊢ ( ∼ Er 𝑋 ↔ ( ◡ 𝐹 ∘ 𝐹 ) Er 𝑋 )
146 143 145 sylibr ⊢ ( 𝜑 → ∼ Er 𝑋 )
147 erssxp ⊢ ( ∼ Er 𝑋 → ∼ ⊆ ( 𝑋 × 𝑋 ) )
148 146 147 syl ⊢ ( 𝜑 → ∼ ⊆ ( 𝑋 × 𝑋 ) )
149 148 138 sseqtrd ⊢ ( 𝜑 → ∼ ⊆ ∪ ( 𝐽 ×t 𝐽 ) )
150 eqid ⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 )
151 150 iscld2 ⊢ ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ ∼ ⊆ ∪ ( 𝐽 ×t 𝐽 ) ) → ( ∼ ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ↔ ( ∪ ( 𝐽 ×t 𝐽 ) ∖ ∼ ) ∈ ( 𝐽 ×t 𝐽 ) ) )
152 141 149 151 syl2anc ⊢ ( 𝜑 → ( ∼ ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ↔ ( ∪ ( 𝐽 ×t 𝐽 ) ∖ ∼ ) ∈ ( 𝐽 ×t 𝐽 ) ) )
153 7 152 mpbid ⊢ ( 𝜑 → ( ∪ ( 𝐽 ×t 𝐽 ) ∖ ∼ ) ∈ ( 𝐽 ×t 𝐽 ) )
154 139 153 eqeltrd ⊢ ( 𝜑 → ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ∈ ( 𝐽 ×t 𝐽 ) )
155 96 96 128 128 130 130 6 136 154 3 txomap ⊢ ( 𝜑 → ( 𝐻 “ ( ( 𝑋 × 𝑋 ) ∖ ∼ ) ) ∈ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
156 126 155 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑌 × 𝑌 ) ∖ ( I ↾ 𝑌 ) ) ∈ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
157 27 156 eqeltrd ⊢ ( 𝜑 → ( ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∖ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) )
158 eqid ⊢ ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) = ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) )
159 158 iscld2 ⊢ ( ( ( ( 𝐽 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 ⊢ ( ( ( ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∈ Top ∧ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ) ∧ ( ∪ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ∖ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ) → ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ) )
161 15 20 157 160 syl21anc ⊢ ( 𝜑 → ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ) )
162 17 hausdiag ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ Haus ↔ ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ ( I ↾ ∪ ( 𝐽 qTop 𝐹 ) ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ×t ( 𝐽 qTop 𝐹 ) ) ) ) )
163 13 161 162 sylanbrc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Haus )