Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  qtophaus Structured version   Visualization version   GIF version

Theorem qtophaus 32474
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.
StepHypRef Expression
1 qtophaus.1 . . . 4 (πœ‘ β†’ 𝐽 ∈ Haus)
2 haustop 22698 . . . 4 (𝐽 ∈ Haus β†’ 𝐽 ∈ Top)
31, 2syl 17 . . 3 (πœ‘ β†’ 𝐽 ∈ Top)
4 qtophaus.2 . . . 4 (πœ‘ β†’ 𝐹:𝑋–ontoβ†’π‘Œ)
5 fofn 6759 . . . 4 (𝐹:𝑋–ontoβ†’π‘Œ β†’ 𝐹 Fn 𝑋)
64, 5syl 17 . . 3 (πœ‘ β†’ 𝐹 Fn 𝑋)
7 qtophaus.x . . . 4 𝑋 = βˆͺ 𝐽
87qtoptop 23067 . . 3 ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) β†’ (𝐽 qTop 𝐹) ∈ Top)
93, 6, 8syl2anc 585 . 2 (πœ‘ β†’ (𝐽 qTop 𝐹) ∈ Top)
10 txtop 22936 . . . 4 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) β†’ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) ∈ Top)
119, 9, 10syl2anc 585 . . 3 (πœ‘ β†’ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) ∈ Top)
12 idssxp 6003 . . . 4 ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) βŠ† (βˆͺ (𝐽 qTop 𝐹) Γ— βˆͺ (𝐽 qTop 𝐹))
13 eqid 2733 . . . . . 6 βˆͺ (𝐽 qTop 𝐹) = βˆͺ (𝐽 qTop 𝐹)
1413, 13txuni 22959 . . . . 5 (((𝐽 qTop 𝐹) ∈ Top ∧ (𝐽 qTop 𝐹) ∈ Top) β†’ (βˆͺ (𝐽 qTop 𝐹) Γ— βˆͺ (𝐽 qTop 𝐹)) = βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
159, 9, 14syl2anc 585 . . . 4 (πœ‘ β†’ (βˆͺ (𝐽 qTop 𝐹) Γ— βˆͺ (𝐽 qTop 𝐹)) = βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
1612, 15sseqtrid 3997 . . 3 (πœ‘ β†’ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) βŠ† βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
177qtopuni 23069 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ π‘Œ = βˆͺ (𝐽 qTop 𝐹))
183, 4, 17syl2anc 585 . . . . . . 7 (πœ‘ β†’ π‘Œ = βˆͺ (𝐽 qTop 𝐹))
1918sqxpeqd 5666 . . . . . 6 (πœ‘ β†’ (π‘Œ Γ— π‘Œ) = (βˆͺ (𝐽 qTop 𝐹) Γ— βˆͺ (𝐽 qTop 𝐹)))
2019, 15eqtr2d 2774 . . . . 5 (πœ‘ β†’ βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) = (π‘Œ Γ— π‘Œ))
2118eqcomd 2739 . . . . . 6 (πœ‘ β†’ βˆͺ (𝐽 qTop 𝐹) = π‘Œ)
2221reseq2d 5938 . . . . 5 (πœ‘ β†’ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) = ( I β†Ύ π‘Œ))
2320, 22difeq12d 4084 . . . 4 (πœ‘ β†’ (βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) βˆ– ( I β†Ύ βˆͺ (𝐽 qTop 𝐹))) = ((π‘Œ Γ— π‘Œ) βˆ– ( I β†Ύ π‘Œ)))
24 qtophaus.h . . . . . . . . . 10 𝐻 = (π‘₯ ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩)
25 opex 5422 . . . . . . . . . 10 ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ V
2624, 25fnmpoi 8003 . . . . . . . . 9 𝐻 Fn (𝑋 Γ— 𝑋)
27 difss 4092 . . . . . . . . 9 ((𝑋 Γ— 𝑋) βˆ– ∼ ) βŠ† (𝑋 Γ— 𝑋)
28 fvelimab 6915 . . . . . . . . 9 ((𝐻 Fn (𝑋 Γ— 𝑋) ∧ ((𝑋 Γ— 𝑋) βˆ– ∼ ) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑐 ∈ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ↔ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐))
2926, 27, 28mp2an 691 . . . . . . . 8 (𝑐 ∈ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ↔ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
30 simp-4r 783 . . . . . . . . . . . . . . . 16 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ π‘₯ ∈ 𝑋)
31 simplr 768 . . . . . . . . . . . . . . . 16 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ 𝑦 ∈ 𝑋)
32 opelxpi 5671 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (𝑋 Γ— 𝑋))
3330, 31, 32syl2anc 585 . . . . . . . . . . . . . . 15 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (𝑋 Γ— 𝑋))
34 df-br 5107 . . . . . . . . . . . . . . 15 (π‘₯(𝑋 Γ— 𝑋)𝑦 ↔ ⟨π‘₯, π‘¦βŸ© ∈ (𝑋 Γ— 𝑋))
3533, 34sylibr 233 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ π‘₯(𝑋 Γ— 𝑋)𝑦)
36 simpllr 775 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (πΉβ€˜π‘₯) = π‘Ž)
37 simpr 486 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (πΉβ€˜π‘¦) = 𝑏)
3836, 37opeq12d 4839 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ = βŸ¨π‘Ž, π‘βŸ©)
39 simp-5r 785 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ 𝑐 = βŸ¨π‘Ž, π‘βŸ©)
40 simp-8r 791 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
4139, 40eqeltrrd 2835 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
4238, 41eqeltrd 2834 . . . . . . . . . . . . . . . . 17 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
43 relxp 5652 . . . . . . . . . . . . . . . . . 18 Rel (π‘Œ Γ— π‘Œ)
44 opeldifid 31563 . . . . . . . . . . . . . . . . . 18 (Rel (π‘Œ Γ— π‘Œ) β†’ (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ) ↔ (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ (π‘Œ Γ— π‘Œ) ∧ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))))
4543, 44ax-mp 5 . . . . . . . . . . . . . . . . 17 (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ) ↔ (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ (π‘Œ Γ— π‘Œ) ∧ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
4642, 45sylib 217 . . . . . . . . . . . . . . . 16 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ (π‘Œ Γ— π‘Œ) ∧ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
4746simprd 497 . . . . . . . . . . . . . . 15 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
486ad8antr 739 . . . . . . . . . . . . . . . . 17 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ 𝐹 Fn 𝑋)
49 qtophaus.e . . . . . . . . . . . . . . . . . 18 ∼ = (◑𝐹 ∘ 𝐹)
5049fcoinvbr 31572 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯ ∼ 𝑦 ↔ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)))
5148, 30, 31, 50syl3anc 1372 . . . . . . . . . . . . . . . 16 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (π‘₯ ∼ 𝑦 ↔ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)))
5251necon3bbid 2978 . . . . . . . . . . . . . . 15 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (Β¬ π‘₯ ∼ 𝑦 ↔ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
5347, 52mpbird 257 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ Β¬ π‘₯ ∼ 𝑦)
54 df-br 5107 . . . . . . . . . . . . . . 15 (π‘₯((𝑋 Γ— 𝑋) βˆ– ∼ )𝑦 ↔ ⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ))
55 brdif 5159 . . . . . . . . . . . . . . 15 (π‘₯((𝑋 Γ— 𝑋) βˆ– ∼ )𝑦 ↔ (π‘₯(𝑋 Γ— 𝑋)𝑦 ∧ Β¬ π‘₯ ∼ 𝑦))
5654, 55bitr3i 277 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ) ↔ (π‘₯(𝑋 Γ— 𝑋)𝑦 ∧ Β¬ π‘₯ ∼ 𝑦))
5735, 53, 56sylanbrc 584 . . . . . . . . . . . . 13 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ ⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ))
5824, 30, 31fvproj 8067 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (π»β€˜βŸ¨π‘₯, π‘¦βŸ©) = ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩)
5938, 58, 393eqtr4d 2783 . . . . . . . . . . . . 13 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ (π»β€˜βŸ¨π‘₯, π‘¦βŸ©) = 𝑐)
60 fveqeq2 6852 . . . . . . . . . . . . . 14 (𝑧 = ⟨π‘₯, π‘¦βŸ© β†’ ((π»β€˜π‘§) = 𝑐 ↔ (π»β€˜βŸ¨π‘₯, π‘¦βŸ©) = 𝑐))
6160rspcev 3580 . . . . . . . . . . . . 13 ((⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ) ∧ (π»β€˜βŸ¨π‘₯, π‘¦βŸ©) = 𝑐) β†’ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
6257, 59, 61syl2anc 585 . . . . . . . . . . . 12 (((((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) ∧ 𝑦 ∈ 𝑋) ∧ (πΉβ€˜π‘¦) = 𝑏) β†’ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
63 fofun 6758 . . . . . . . . . . . . . . . 16 (𝐹:𝑋–ontoβ†’π‘Œ β†’ Fun 𝐹)
644, 63syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Fun 𝐹)
6564ad4antr 731 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ Fun 𝐹)
6665ad2antrr 725 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ Fun 𝐹)
67 simp-4r 783 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ 𝑏 ∈ π‘Œ)
68 foima 6762 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋–ontoβ†’π‘Œ β†’ (𝐹 β€œ 𝑋) = π‘Œ)
694, 68syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹 β€œ 𝑋) = π‘Œ)
7069ad4antr 731 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ (𝐹 β€œ 𝑋) = π‘Œ)
7170ad2antrr 725 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ (𝐹 β€œ 𝑋) = π‘Œ)
7267, 71eleqtrrd 2837 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ 𝑏 ∈ (𝐹 β€œ 𝑋))
73 fvelima 6909 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ 𝑏 ∈ (𝐹 β€œ 𝑋)) β†’ βˆƒπ‘¦ ∈ 𝑋 (πΉβ€˜π‘¦) = 𝑏)
7466, 72, 73syl2anc 585 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ βˆƒπ‘¦ ∈ 𝑋 (πΉβ€˜π‘¦) = 𝑏)
7562, 74r19.29a 3156 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) ∧ π‘₯ ∈ 𝑋) ∧ (πΉβ€˜π‘₯) = π‘Ž) β†’ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
76 simpllr 775 . . . . . . . . . . . . 13 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ π‘Ž ∈ π‘Œ)
7776, 70eleqtrrd 2837 . . . . . . . . . . . 12 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ π‘Ž ∈ (𝐹 β€œ 𝑋))
78 fvelima 6909 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ π‘Ž ∈ (𝐹 β€œ 𝑋)) β†’ βˆƒπ‘₯ ∈ 𝑋 (πΉβ€˜π‘₯) = π‘Ž)
7965, 77, 78syl2anc 585 . . . . . . . . . . 11 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ βˆƒπ‘₯ ∈ 𝑋 (πΉβ€˜π‘₯) = π‘Ž)
8075, 79r19.29a 3156 . . . . . . . . . 10 (((((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) ∧ π‘Ž ∈ π‘Œ) ∧ 𝑏 ∈ π‘Œ) ∧ 𝑐 = βŸ¨π‘Ž, π‘βŸ©) β†’ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
81 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) β†’ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
8281eldifad 3923 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) β†’ 𝑐 ∈ (π‘Œ Γ— π‘Œ))
83 elxp2 5658 . . . . . . . . . . 11 (𝑐 ∈ (π‘Œ Γ— π‘Œ) ↔ βˆƒπ‘Ž ∈ π‘Œ βˆƒπ‘ ∈ π‘Œ 𝑐 = βŸ¨π‘Ž, π‘βŸ©)
8482, 83sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) β†’ βˆƒπ‘Ž ∈ π‘Œ βˆƒπ‘ ∈ π‘Œ 𝑐 = βŸ¨π‘Ž, π‘βŸ©)
8580, 84r19.29vva 3204 . . . . . . . . 9 ((πœ‘ ∧ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )) β†’ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐)
86 simpr 486 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝑧 = ⟨π‘₯, π‘¦βŸ©)
8786fveq2d 6847 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (π»β€˜π‘§) = (π»β€˜βŸ¨π‘₯, π‘¦βŸ©))
88 simp-4r 783 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (π»β€˜π‘§) = 𝑐)
89 simpllr 775 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ π‘₯ ∈ 𝑋)
90 simplr 768 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝑦 ∈ 𝑋)
9124, 89, 90fvproj 8067 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (π»β€˜βŸ¨π‘₯, π‘¦βŸ©) = ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩)
9287, 88, 913eqtr3d 2781 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝑐 = ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩)
93 fof 6757 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋–ontoβ†’π‘Œ β†’ 𝐹:π‘‹βŸΆπ‘Œ)
944, 93syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π‘‹βŸΆπ‘Œ)
9594ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
9695, 89ffvelcdmd 7037 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (πΉβ€˜π‘₯) ∈ π‘Œ)
9795, 90ffvelcdmd 7037 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (πΉβ€˜π‘¦) ∈ π‘Œ)
98 opelxp 5670 . . . . . . . . . . . . . 14 (⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ (π‘Œ Γ— π‘Œ) ↔ ((πΉβ€˜π‘₯) ∈ π‘Œ ∧ (πΉβ€˜π‘¦) ∈ π‘Œ))
9996, 97, 98sylanbrc 584 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ (π‘Œ Γ— π‘Œ))
100 simp-5r 785 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ))
10186, 100eqeltrrd 2835 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ ⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ))
10256simprbi 498 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ) β†’ Β¬ π‘₯ ∼ 𝑦)
103101, 102syl 17 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ Β¬ π‘₯ ∼ 𝑦)
1046ad5antr 733 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝐹 Fn 𝑋)
105104, 89, 90, 50syl3anc 1372 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (π‘₯ ∼ 𝑦 ↔ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦)))
106105necon3bbid 2978 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (Β¬ π‘₯ ∼ 𝑦 ↔ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦)))
107103, 106mpbid 231 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ (πΉβ€˜π‘₯) β‰  (πΉβ€˜π‘¦))
10899, 107, 45sylanbrc 584 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ ⟨(πΉβ€˜π‘₯), (πΉβ€˜π‘¦)⟩ ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
10992, 108eqeltrd 2834 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 = ⟨π‘₯, π‘¦βŸ©) β†’ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
110 eldifi 4087 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ ) β†’ 𝑧 ∈ (𝑋 Γ— 𝑋))
111110adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) β†’ 𝑧 ∈ (𝑋 Γ— 𝑋))
112 elxp2 5658 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 Γ— 𝑋) ↔ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝑋 𝑧 = ⟨π‘₯, π‘¦βŸ©)
113111, 112sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝑋 𝑧 = ⟨π‘₯, π‘¦βŸ©)
114113adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) β†’ βˆƒπ‘₯ ∈ 𝑋 βˆƒπ‘¦ ∈ 𝑋 𝑧 = ⟨π‘₯, π‘¦βŸ©)
115109, 114r19.29vva 3204 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∧ (π»β€˜π‘§) = 𝑐) β†’ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
116115r19.29an 3152 . . . . . . . . 9 ((πœ‘ ∧ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐) β†’ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ))
11785, 116impbida 800 . . . . . . . 8 (πœ‘ β†’ (𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I ) ↔ βˆƒπ‘§ ∈ ((𝑋 Γ— 𝑋) βˆ– ∼ )(π»β€˜π‘§) = 𝑐))
11829, 117bitr4id 290 . . . . . . 7 (πœ‘ β†’ (𝑐 ∈ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ↔ 𝑐 ∈ ((π‘Œ Γ— π‘Œ) βˆ– I )))
119118eqrdv 2731 . . . . . 6 (πœ‘ β†’ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) = ((π‘Œ Γ— π‘Œ) βˆ– I ))
120 ssv 3969 . . . . . . 7 π‘Œ βŠ† V
121 xpss2 5654 . . . . . . 7 (π‘Œ βŠ† V β†’ (π‘Œ Γ— π‘Œ) βŠ† (π‘Œ Γ— V))
122 difres 31564 . . . . . . 7 ((π‘Œ Γ— π‘Œ) βŠ† (π‘Œ Γ— V) β†’ ((π‘Œ Γ— π‘Œ) βˆ– ( I β†Ύ π‘Œ)) = ((π‘Œ Γ— π‘Œ) βˆ– I ))
123120, 121, 122mp2b 10 . . . . . 6 ((π‘Œ Γ— π‘Œ) βˆ– ( I β†Ύ π‘Œ)) = ((π‘Œ Γ— π‘Œ) βˆ– I )
124119, 123eqtr4di 2791 . . . . 5 (πœ‘ β†’ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) = ((π‘Œ Γ— π‘Œ) βˆ– ( I β†Ύ π‘Œ)))
1257toptopon 22282 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
1263, 125sylib 217 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
127 qtoptopon 23071 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ (𝐽 qTop 𝐹) ∈ (TopOnβ€˜π‘Œ))
128126, 4, 127syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝐽 qTop 𝐹) ∈ (TopOnβ€˜π‘Œ))
129 qtophaus.3 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐽) β†’ (𝐹 β€œ π‘₯) ∈ (𝐽 qTop 𝐹))
130129ralrimiva 3140 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐽 (𝐹 β€œ π‘₯) ∈ (𝐽 qTop 𝐹))
131 imaeq2 6010 . . . . . . . . . 10 (π‘₯ = 𝑦 β†’ (𝐹 β€œ π‘₯) = (𝐹 β€œ 𝑦))
132131eleq1d 2819 . . . . . . . . 9 (π‘₯ = 𝑦 β†’ ((𝐹 β€œ π‘₯) ∈ (𝐽 qTop 𝐹) ↔ (𝐹 β€œ 𝑦) ∈ (𝐽 qTop 𝐹)))
133132cbvralvw 3224 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝐽 (𝐹 β€œ π‘₯) ∈ (𝐽 qTop 𝐹) ↔ βˆ€π‘¦ ∈ 𝐽 (𝐹 β€œ 𝑦) ∈ (𝐽 qTop 𝐹))
134130, 133sylib 217 . . . . . . 7 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝐽 (𝐹 β€œ 𝑦) ∈ (𝐽 qTop 𝐹))
135134r19.21bi 3233 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐽) β†’ (𝐹 β€œ 𝑦) ∈ (𝐽 qTop 𝐹))
1367, 7txuni 22959 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
1373, 3, 136syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
138137difeq1d 4082 . . . . . . 7 (πœ‘ β†’ ((𝑋 Γ— 𝑋) βˆ– ∼ ) = (βˆͺ (𝐽 Γ—t 𝐽) βˆ– ∼ ))
139 qtophaus.4 . . . . . . . 8 (πœ‘ β†’ ∼ ∈ (Clsdβ€˜(𝐽 Γ—t 𝐽)))
140 txtop 22936 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
1413, 3, 140syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (𝐽 Γ—t 𝐽) ∈ Top)
142 fcoinver 31571 . . . . . . . . . . . . 13 (𝐹 Fn 𝑋 β†’ (◑𝐹 ∘ 𝐹) Er 𝑋)
1436, 142syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (◑𝐹 ∘ 𝐹) Er 𝑋)
144 ereq1 8658 . . . . . . . . . . . . 13 ( ∼ = (◑𝐹 ∘ 𝐹) β†’ ( ∼ Er 𝑋 ↔ (◑𝐹 ∘ 𝐹) Er 𝑋))
14549, 144ax-mp 5 . . . . . . . . . . . 12 ( ∼ Er 𝑋 ↔ (◑𝐹 ∘ 𝐹) Er 𝑋)
146143, 145sylibr 233 . . . . . . . . . . 11 (πœ‘ β†’ ∼ Er 𝑋)
147 erssxp 8674 . . . . . . . . . . 11 ( ∼ Er 𝑋 β†’ ∼ βŠ† (𝑋 Γ— 𝑋))
148146, 147syl 17 . . . . . . . . . 10 (πœ‘ β†’ ∼ βŠ† (𝑋 Γ— 𝑋))
149148, 137sseqtrd 3985 . . . . . . . . 9 (πœ‘ β†’ ∼ βŠ† βˆͺ (𝐽 Γ—t 𝐽))
150 eqid 2733 . . . . . . . . . 10 βˆͺ (𝐽 Γ—t 𝐽) = βˆͺ (𝐽 Γ—t 𝐽)
151150iscld2 22395 . . . . . . . . 9 (((𝐽 Γ—t 𝐽) ∈ Top ∧ ∼ βŠ† βˆͺ (𝐽 Γ—t 𝐽)) β†’ ( ∼ ∈ (Clsdβ€˜(𝐽 Γ—t 𝐽)) ↔ (βˆͺ (𝐽 Γ—t 𝐽) βˆ– ∼ ) ∈ (𝐽 Γ—t 𝐽)))
152141, 149, 151syl2anc 585 . . . . . . . 8 (πœ‘ β†’ ( ∼ ∈ (Clsdβ€˜(𝐽 Γ—t 𝐽)) ↔ (βˆͺ (𝐽 Γ—t 𝐽) βˆ– ∼ ) ∈ (𝐽 Γ—t 𝐽)))
153139, 152mpbid 231 . . . . . . 7 (πœ‘ β†’ (βˆͺ (𝐽 Γ—t 𝐽) βˆ– ∼ ) ∈ (𝐽 Γ—t 𝐽))
154138, 153eqeltrd 2834 . . . . . 6 (πœ‘ β†’ ((𝑋 Γ— 𝑋) βˆ– ∼ ) ∈ (𝐽 Γ—t 𝐽))
15594, 94, 126, 126, 128, 128, 129, 135, 154, 24txomap 32472 . . . . 5 (πœ‘ β†’ (𝐻 β€œ ((𝑋 Γ— 𝑋) βˆ– ∼ )) ∈ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
156124, 155eqeltrrd 2835 . . . 4 (πœ‘ β†’ ((π‘Œ Γ— π‘Œ) βˆ– ( I β†Ύ π‘Œ)) ∈ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
15723, 156eqeltrd 2834 . . 3 (πœ‘ β†’ (βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) βˆ– ( I β†Ύ βˆͺ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))
158 eqid 2733 . . . . 5 βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) = βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))
159158iscld2 22395 . . . 4 ((((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) βŠ† βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))) β†’ (( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) ∈ (Clsdβ€˜((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))) ↔ (βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) βˆ– ( I β†Ύ βˆͺ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))))
160159biimpar 479 . . 3 (((((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) ∈ Top ∧ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) βŠ† βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))) ∧ (βˆͺ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)) βˆ– ( I β†Ύ βˆͺ (𝐽 qTop 𝐹))) ∈ ((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))) β†’ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) ∈ (Clsdβ€˜((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))))
16111, 16, 157, 160syl21anc 837 . 2 (πœ‘ β†’ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) ∈ (Clsdβ€˜((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹))))
16213hausdiag 23012 . 2 ((𝐽 qTop 𝐹) ∈ Haus ↔ ((𝐽 qTop 𝐹) ∈ Top ∧ ( I β†Ύ βˆͺ (𝐽 qTop 𝐹)) ∈ (Clsdβ€˜((𝐽 qTop 𝐹) Γ—t (𝐽 qTop 𝐹)))))
1639, 161, 162sylanbrc 584 1 (πœ‘ β†’ (𝐽 qTop 𝐹) ∈ Haus)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   βŠ† wss 3911  βŸ¨cop 4593  βˆͺ cuni 4866   class class class wbr 5106   I cid 5531   Γ— cxp 5632  β—‘ccnv 5633   β†Ύ cres 5636   β€œ cima 5637   ∘ ccom 5638  Rel wrel 5639  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“ontoβ†’wfo 6495  β€˜cfv 6497  (class class class)co 7358   ∈ cmpo 7360   Er wer 8648   qTop cqtop 17390  Topctop 22258  TopOnctopon 22275  Clsdccld 22383  Hauscha 22675   Γ—t ctx 22927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-er 8651  df-topgen 17330  df-qtop 17394  df-top 22259  df-topon 22276  df-bases 22312  df-cld 22386  df-haus 22682  df-tx 22929
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator