Theorem pr2dom

Description: An unordered pair is dominated by ordinal two. (Contributed by RP, 29-Oct-2023)

	Ref	Expression
Assertion	pr2dom	$$⊢\left\{A,B\right\}\preccurlyeq 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
4		undjudom	$$⊢\left(\left\{A\right\}\in \mathrm{V}\wedge \left\{B\right\}\in \mathrm{V}\right)\to \left(\left\{A\right\}\cup \left\{B\right\}\right)\preccurlyeq \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)$$
5	2 3 4	mp2an	$$⊢\left(\left\{A\right\}\cup \left\{B\right\}\right)\preccurlyeq \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)$$
6		sn1dom	$$⊢\left\{A\right\}\preccurlyeq 1_{𝑜}$$
7		djudom1	$$⊢\left(\left\{A\right\}\preccurlyeq 1_{𝑜}\wedge \left\{B\right\}\in \mathrm{V}\right)\to \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)$$
8	6 3 7	mp2an	$$⊢\left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)$$
9		sn1dom	$$⊢\left\{B\right\}\preccurlyeq 1_{𝑜}$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11		djudom2	$$⊢\left(\left\{B\right\}\preccurlyeq 1_{𝑜}\wedge 1_{𝑜}\in \mathrm{On}\right)\to \left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
12	9 10 11	mp2an	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
13		domtr	$$⊢\left(\left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\wedge \left(1_{𝑜}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)\to \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
14	8 12 13	mp2an	$$⊢\left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
15		dju1p1e2	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}$$
16		domentr	$$⊢\left(\left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\wedge \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}\right)\to \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq 2_{𝑜}$$
17	14 15 16	mp2an	$$⊢\left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq 2_{𝑜}$$
18		domtr	$$⊢\left(\left(\left\{A\right\}\cup \left\{B\right\}\right)\preccurlyeq \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\wedge \left(\left\{A\right\}\mathrm{\bigsqcup ︀}\left\{B\right\}\right)\preccurlyeq 2_{𝑜}\right)\to \left(\left\{A\right\}\cup \left\{B\right\}\right)\preccurlyeq 2_{𝑜}$$
19	5 17 18	mp2an	$$⊢\left(\left\{A\right\}\cup \left\{B\right\}\right)\preccurlyeq 2_{𝑜}$$
20	1 19	eqbrtri	$$⊢\left\{A,B\right\}\preccurlyeq 2_{𝑜}$$