Metamath Proof Explorer


Theorem pr2dom

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

Ref Expression
Assertion pr2dom A B 2 𝑜

Proof

Step Hyp Ref Expression
1 df-pr A B = A B
2 snex A V
3 snex B V
4 undjudom A V B V A B A ⊔︀ B
5 2 3 4 mp2an A B A ⊔︀ B
6 sn1dom A 1 𝑜
7 djudom1 A 1 𝑜 B V A ⊔︀ B 1 𝑜 ⊔︀ B
8 6 3 7 mp2an A ⊔︀ B 1 𝑜 ⊔︀ B
9 sn1dom B 1 𝑜
10 1on 1 𝑜 On
11 djudom2 B 1 𝑜 1 𝑜 On 1 𝑜 ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜
12 9 10 11 mp2an 1 𝑜 ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜
13 domtr A ⊔︀ B 1 𝑜 ⊔︀ B 1 𝑜 ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜 A ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜
14 8 12 13 mp2an A ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜
15 dju1p1e2 1 𝑜 ⊔︀ 1 𝑜 2 𝑜
16 domentr A ⊔︀ B 1 𝑜 ⊔︀ 1 𝑜 1 𝑜 ⊔︀ 1 𝑜 2 𝑜 A ⊔︀ B 2 𝑜
17 14 15 16 mp2an A ⊔︀ B 2 𝑜
18 domtr A B A ⊔︀ B A ⊔︀ B 2 𝑜 A B 2 𝑜
19 5 17 18 mp2an A B 2 𝑜
20 1 19 eqbrtri A B 2 𝑜