Metamath Proof Explorer

Theorem txswaphmeo

Description: There is a homeomorphism from X X. Y to Y X. X . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion txswaphmeo ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( 𝐾 ×t 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 1 2 cnmpt2nd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
4 1 2 cnmpt1st ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
5 1 2 3 4 cnmpt2t ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐾 ×t 𝐽 ) ) )
6 opelxpi ⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
7 6 ancoms ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
8 7 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
9 8 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ )
11 10 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) ⟶ ( 𝑌 × 𝑋 ) )
12 9 11 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) ⟶ ( 𝑌 × 𝑋 ) )
13 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
14 13 ancoms ⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
15 14 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
16 15 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
17 eqid ⊢ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
18 17 fmpo ⊢ ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) : ( 𝑌 × 𝑋 ) ⟶ ( 𝑋 × 𝑌 ) )
19 16 18 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) : ( 𝑌 × 𝑋 ) ⟶ ( 𝑋 × 𝑌 ) )
20 txswaphmeolem ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∘ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( I ↾ ( 𝑌 × 𝑋 ) )
21 txswaphmeolem ⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) )
22 fcof1o ⊢ ( ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) ⟶ ( 𝑌 × 𝑋 ) ∧ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) : ( 𝑌 × 𝑋 ) ⟶ ( 𝑋 × 𝑌 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∘ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( I ↾ ( 𝑌 × 𝑋 ) ) ∧ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) ) ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ( 𝑌 × 𝑋 ) ∧ ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
23 20 21 22 mpanr12 ⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) ⟶ ( 𝑌 × 𝑋 ) ∧ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) : ( 𝑌 × 𝑋 ) ⟶ ( 𝑋 × 𝑌 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ( 𝑌 × 𝑋 ) ∧ ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
24 12 19 23 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ( 𝑌 × 𝑋 ) ∧ ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
25 24 simprd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) )
26 2 1 cnmpt2nd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
27 2 1 cnmpt1st ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ 𝑦 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐾 ) )
28 2 1 26 27 cnmpt2t ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn ( 𝐽 ×t 𝐾 ) ) )
29 25 28 eqeltrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn ( 𝐽 ×t 𝐾 ) ) )
30 ishmeo ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( 𝐾 ×t 𝐽 ) ) ↔ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐾 ×t 𝐽 ) ) ∧ ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn ( 𝐽 ×t 𝐾 ) ) ) )
31 5 29 30 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Homeo ( 𝐾 ×t 𝐽 ) ) )