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	|- ( ph -> A e. C )
	enpr2d.2	|- ( ph -> B e. D )
	enpr2d.3	|- ( ph -> -. A = B )
Assertion	enpr2d	|- ( ph -> { A , B } ~~ 2o )

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	|- ( ph -> A e. C )
2		enpr2d.2	|- ( ph -> B e. D )
3		enpr2d.3	|- ( ph -> -. A = B )
4		ensn1g	|- ( A e. C -> { A } ~~ 1o )
5	1 4	syl	|- ( ph -> { A } ~~ 1o )
6		1on	|- 1o e. On
7		en2sn	|- ( ( B e. D /\ 1o e. On ) -> { B } ~~ { 1o } )
8	2 6 7	sylancl	|- ( ph -> { B } ~~ { 1o } )
9	3	neqned	|- ( ph -> A =/= B )
10		disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
11	9 10	syl	|- ( ph -> ( { A } i^i { B } ) = (/) )
12	6	onirri	|- -. 1o e. 1o
13	12	a1i	|- ( ph -> -. 1o e. 1o )
14		disjsn	|- ( ( 1o i^i { 1o } ) = (/) <-> -. 1o e. 1o )
15	13 14	sylibr	|- ( ph -> ( 1o i^i { 1o } ) = (/) )
16		unen	|- ( ( ( { A } ~~ 1o /\ { B } ~~ { 1o } ) /\ ( ( { A } i^i { B } ) = (/) /\ ( 1o i^i { 1o } ) = (/) ) ) -> ( { A } u. { B } ) ~~ ( 1o u. { 1o } ) )
17	5 8 11 15 16	syl22anc	|- ( ph -> ( { A } u. { B } ) ~~ ( 1o u. { 1o } ) )
18		df-pr	|- { A , B } = ( { A } u. { B } )
19		df-suc	|- suc 1o = ( 1o u. { 1o } )
20	17 18 19	3brtr4g	|- ( ph -> { A , B } ~~ suc 1o )
21		df-2o	|- 2o = suc 1o
22	20 21	breqtrrdi	|- ( ph -> { A , B } ~~ 2o )