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	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ { 𝐶 , 𝐷 } )