This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1oprg

Description: An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap . (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion f1oprg ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐴 , 𝐶 } –1-1-onto→ { 𝐵 , 𝐷 } ) )

Proof

Step Hyp Ref Expression
1 f1osng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )
2 1 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )
3 f1osng ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → { ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐶 } –1-1-onto→ { 𝐷 } )
4 3 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐶 } –1-1-onto→ { 𝐷 } )
5 disjsn2 ⊢ ( 𝐴 ≠ 𝐶 → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
6 5 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 } ∩ { 𝐶 } ) = ∅ )
7 disjsn2 ⊢ ( 𝐵 ≠ 𝐷 → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
8 7 ad2antll ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐵 } ∩ { 𝐷 } ) = ∅ )
9 f1oun ⊢ ( ( ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ∧ { ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐶 } –1-1-onto→ { 𝐷 } ) ∧ ( ( { 𝐴 } ∩ { 𝐶 } ) = ∅ ∧ ( { 𝐵 } ∩ { 𝐷 } ) = ∅ ) ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) : ( { 𝐴 } ∪ { 𝐶 } ) –1-1-onto→ ( { 𝐵 } ∪ { 𝐷 } ) )
10 2 4 6 8 9 syl22anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) : ( { 𝐴 } ∪ { 𝐶 } ) –1-1-onto→ ( { 𝐵 } ∪ { 𝐷 } ) )
11 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
12 11 eqcomi ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ }
13 12 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } )
14 df-pr ⊢ { 𝐴 , 𝐶 } = ( { 𝐴 } ∪ { 𝐶 } )
15 14 eqcomi ⊢ ( { 𝐴 } ∪ { 𝐶 } ) = { 𝐴 , 𝐶 }
16 15 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐴 } ∪ { 𝐶 } ) = { 𝐴 , 𝐶 } )
17 df-pr ⊢ { 𝐵 , 𝐷 } = ( { 𝐵 } ∪ { 𝐷 } )
18 17 eqcomi ⊢ ( { 𝐵 } ∪ { 𝐷 } ) = { 𝐵 , 𝐷 }
19 18 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( { 𝐵 } ∪ { 𝐷 } ) = { 𝐵 , 𝐷 } )
20 13 16 19 f1oeq123d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) : ( { 𝐴 } ∪ { 𝐶 } ) –1-1-onto→ ( { 𝐵 } ∪ { 𝐷 } ) ↔ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐴 , 𝐶 } –1-1-onto→ { 𝐵 , 𝐷 } ) )
21 10 20 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐴 , 𝐶 } –1-1-onto→ { 𝐵 , 𝐷 } )
22 21 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } : { 𝐴 , 𝐶 } –1-1-onto→ { 𝐵 , 𝐷 } ) )