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→ { 𝐵 , 𝐷 } ) )