Metamath Proof Explorer


Theorem pr2dom

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

Ref Expression
Assertion pr2dom AB2𝑜

Proof

Step Hyp Ref Expression
1 df-pr AB=AB
2 snex AV
3 snex BV
4 undjudom AVBVABA⊔︀B
5 2 3 4 mp2an ABA⊔︀B
6 sn1dom A1𝑜
7 djudom1 A1𝑜BVA⊔︀B1𝑜⊔︀B
8 6 3 7 mp2an A⊔︀B1𝑜⊔︀B
9 sn1dom B1𝑜
10 1on 1𝑜On
11 djudom2 B1𝑜1𝑜On1𝑜⊔︀B1𝑜⊔︀1𝑜
12 9 10 11 mp2an 1𝑜⊔︀B1𝑜⊔︀1𝑜
13 domtr A⊔︀B1𝑜⊔︀B1𝑜⊔︀B1𝑜⊔︀1𝑜A⊔︀B1𝑜⊔︀1𝑜
14 8 12 13 mp2an A⊔︀B1𝑜⊔︀1𝑜
15 dju1p1e2 1𝑜⊔︀1𝑜2𝑜
16 domentr A⊔︀B1𝑜⊔︀1𝑜1𝑜⊔︀1𝑜2𝑜A⊔︀B2𝑜
17 14 15 16 mp2an A⊔︀B2𝑜
18 domtr ABA⊔︀BA⊔︀B2𝑜AB2𝑜
19 5 17 18 mp2an AB2𝑜
20 1 19 eqbrtri AB2𝑜