Metamath Proof Explorer

Theorem f1oprswap

Description: A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Assertion f1oprswap ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } )

Proof

Step Hyp Ref Expression
1 f1osng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → { ⟨ 𝐴 , 𝐴 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐴 } )
2 1 anidms ⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝐴 , 𝐴 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐴 } )
3 2 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → { ⟨ 𝐴 , 𝐴 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐴 } )
4 dfsn2 ⊢ { ⟨ 𝐴 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐴 , 𝐴 ⟩ }
5 opeq2 ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐴 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
6 opeq1 ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐴 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ )
7 5 6 preq12d ⊢ ( 𝐴 = 𝐵 → { ⟨ 𝐴 , 𝐴 ⟩ , ⟨ 𝐴 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } )
8 4 7 eqtrid ⊢ ( 𝐴 = 𝐵 → { ⟨ 𝐴 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } )
9 dfsn2 ⊢ { 𝐴 } = { 𝐴 , 𝐴 }
10 preq2 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
11 9 10 eqtrid ⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐴 , 𝐵 } )
12 8 11 11 f1oeq123d ⊢ ( 𝐴 = 𝐵 → ( { ⟨ 𝐴 , 𝐴 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐴 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → ( { ⟨ 𝐴 , 𝐴 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐴 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } ) )
14 3 13 mpbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 = 𝐵 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } )
15 simpll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑉 )
16 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑊 )
17 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
18 fnprg ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } )
19 15 16 16 15 17 18 syl221anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } )
20 cnvsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ } )
21 cnvsng ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
22 21 ancoms ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
23 20 22 uneq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } ) = ( { ⟨ 𝐵 , 𝐴 ⟩ } ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
24 uncom ⊢ ( { ⟨ 𝐵 , 𝐴 ⟩ } ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } )
25 23 24 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } ) )
26 25 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } ) )
27 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } )
28 27 cnveqi ⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } = ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } )
29 cnvun ⊢ ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐵 , 𝐴 ⟩ } ) = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } )
30 28 29 eqtri ⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } )
31 26 30 27 3eqtr4g ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } )
32 31 fneq1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } ) )
33 19 32 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } )
34 dff1o4 ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } ↔ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } ∧ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐴 , 𝐵 } ) )
35 19 33 34 sylanbrc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } )
36 14 35 pm2.61dane ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐴 , 𝐵 } )