Theorem enpr2d

Description: A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	enpr2d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	enpr2d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	enpr2d.3	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
Assertion	enpr2d	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		enpr2d.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		enpr2d.3	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
4		ensn1g	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 } ≈ 1o )
5	1 4	syl	⊢ ( 𝜑 → { 𝐴 } ≈ 1o )
6		1on	⊢ 1o ∈ On
7		en2sn	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 1o ∈ On ) → { 𝐵 } ≈ { 1o } )
8	2 6 7	sylancl	⊢ ( 𝜑 → { 𝐵 } ≈ { 1o } )
9	3	neqned	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
10		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
11	9 10	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
12	6	onirri	⊢ ¬ 1o ∈ 1o
13	12	a1i	⊢ ( 𝜑 → ¬ 1o ∈ 1o )
14		disjsn	⊢ ( ( 1o ∩ { 1o } ) = ∅ ↔ ¬ 1o ∈ 1o )
15	13 14	sylibr	⊢ ( 𝜑 → ( 1o ∩ { 1o } ) = ∅ )
16		unen	⊢ ( ( ( { 𝐴 } ≈ 1o ∧ { 𝐵 } ≈ { 1o } ) ∧ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ∧ ( 1o ∩ { 1o } ) = ∅ ) ) → ( { 𝐴 } ∪ { 𝐵 } ) ≈ ( 1o ∪ { 1o } ) )
17	5 8 11 15 16	syl22anc	⊢ ( 𝜑 → ( { 𝐴 } ∪ { 𝐵 } ) ≈ ( 1o ∪ { 1o } ) )
18		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
19		df-suc	⊢ suc 1o = ( 1o ∪ { 1o } )
20	17 18 19	3brtr4g	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ suc 1o )
21		df-2o	⊢ 2o = suc 1o
22	20 21	breqtrrdi	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≈ 2o )