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	$$⊢\phi \to A\in C$$
	enpr2d.2	$$⊢\phi \to B\in D$$
	enpr2d.3	$$⊢\phi \to \neg A=B$$
Assertion	enpr2d	$$⊢\phi \to \left\{A,B\right\}\approx 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	$$⊢\phi \to A\in C$$
2		enpr2d.2	$$⊢\phi \to B\in D$$
3		enpr2d.3	$$⊢\phi \to \neg A=B$$
4		ensn1g	$$⊢A\in C\to \left\{A\right\}\approx 1_{𝑜}$$
5	1 4	syl	$$⊢\phi \to \left\{A\right\}\approx 1_{𝑜}$$
6		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
7		en2sn	$$⊢\left(B\in D\wedge 1_{𝑜}\in \mathrm{On}\right)\to \left\{B\right\}\approx \left\{1_{𝑜}\right\}$$
8	2 6 7	sylancl	$$⊢\phi \to \left\{B\right\}\approx \left\{1_{𝑜}\right\}$$
9	3	neqned	$$⊢\phi \to A\ne B$$
10		disjsn2	$$⊢A\ne B\to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
11	9 10	syl	$$⊢\phi \to \left\{A\right\}\cap \left\{B\right\}=\varnothing$$
12	6	onirri	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
13	12	a1i	$$⊢\phi \to \neg 1_{𝑜}\in 1_{𝑜}$$
14		disjsn	$$⊢1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing \leftrightarrow \neg 1_{𝑜}\in 1_{𝑜}$$
15	13 14	sylibr	$$⊢\phi \to 1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing$$
16		unen	$$⊢\left(\left(\left\{A\right\}\approx 1_{𝑜}\wedge \left\{B\right\}\approx \left\{1_{𝑜}\right\}\right)\wedge \left(\left\{A\right\}\cap \left\{B\right\}=\varnothing \wedge 1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing \right)\right)\to \left(\left\{A\right\}\cup \left\{B\right\}\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)$$
17	5 8 11 15 16	syl22anc	$$⊢\phi \to \left(\left\{A\right\}\cup \left\{B\right\}\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)$$
18		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
19		df-suc	$$⊢\mathrm{suc}{1}_{𝑜}=1_{𝑜}\cup \left\{1_{𝑜}\right\}$$
20	17 18 19	3brtr4g	$$⊢\phi \to \left\{A,B\right\}\approx \mathrm{suc}{1}_{𝑜}$$
21		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
22	20 21	breqtrrdi	$$⊢\phi \to \left\{A,B\right\}\approx 2_{𝑜}$$