Metamath Proof Explorer


Theorem en2prd

Description: Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024)

Ref Expression
Hypotheses en2prd.1 ( 𝜑𝐴𝑉 )
en2prd.2 ( 𝜑𝐵𝑊 )
en2prd.3 ( 𝜑𝐶𝑋 )
en2prd.4 ( 𝜑𝐷𝑌 )
en2prd.5 ( 𝜑𝐴𝐵 )
en2prd.6 ( 𝜑𝐶𝐷 )
Assertion en2prd ( 𝜑 → { 𝐴 , 𝐵 } ≈ { 𝐶 , 𝐷 } )

Proof

Step Hyp Ref Expression
1 en2prd.1 ( 𝜑𝐴𝑉 )
2 en2prd.2 ( 𝜑𝐵𝑊 )
3 en2prd.3 ( 𝜑𝐶𝑋 )
4 en2prd.4 ( 𝜑𝐷𝑌 )
5 en2prd.5 ( 𝜑𝐴𝐵 )
6 en2prd.6 ( 𝜑𝐶𝐷 )
7 prex { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∈ V
8 f1oprg ( ( ( 𝐴𝑉𝐶𝑋 ) ∧ ( 𝐵𝑊𝐷𝑌 ) ) → ( ( 𝐴𝐵𝐶𝐷 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
9 1 3 2 4 8 syl22anc ( 𝜑 → ( ( 𝐴𝐵𝐶𝐷 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
10 5 6 9 mp2and ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } )
11 f1oeq1 ( 𝑓 = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } → ( 𝑓 : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ↔ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
12 11 spcegv ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∈ V → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } → ∃ 𝑓 𝑓 : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
13 7 10 12 mpsyl ( 𝜑 → ∃ 𝑓 𝑓 : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } )
14 prex { 𝐴 , 𝐵 } ∈ V
15 prex { 𝐶 , 𝐷 } ∈ V
16 breng ( ( { 𝐴 , 𝐵 } ∈ V ∧ { 𝐶 , 𝐷 } ∈ V ) → ( { 𝐴 , 𝐵 } ≈ { 𝐶 , 𝐷 } ↔ ∃ 𝑓 𝑓 : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } ) )
17 14 15 16 mp2an ( { 𝐴 , 𝐵 } ≈ { 𝐶 , 𝐷 } ↔ ∃ 𝑓 𝑓 : { 𝐴 , 𝐵 } –1-1-onto→ { 𝐶 , 𝐷 } )
18 13 17 sylibr ( 𝜑 → { 𝐴 , 𝐵 } ≈ { 𝐶 , 𝐷 } )