Metamath Proof Explorer


Theorem tr3dom

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

Ref Expression
Assertion tr3dom A B C 3 𝑜

Proof

Step Hyp Ref Expression
1 df-tp A B C = A B C
2 prex A B V
3 snex C V
4 undjudom A B V C V A B C A B ⊔︀ C
5 2 3 4 mp2an A B C A B ⊔︀ C
6 pr2dom A B 2 𝑜
7 djudom1 A B 2 𝑜 C V A B ⊔︀ C 2 𝑜 ⊔︀ C
8 6 3 7 mp2an A B ⊔︀ C 2 𝑜 ⊔︀ C
9 sn1dom C 1 𝑜
10 2on 2 𝑜 On
11 djudom2 C 1 𝑜 2 𝑜 On 2 𝑜 ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜
12 9 10 11 mp2an 2 𝑜 ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜
13 domtr A B ⊔︀ C 2 𝑜 ⊔︀ C 2 𝑜 ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜 A B ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜
14 8 12 13 mp2an A B ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜
15 1on 1 𝑜 On
16 onadju 2 𝑜 On 1 𝑜 On 2 𝑜 + 𝑜 1 𝑜 2 𝑜 ⊔︀ 1 𝑜
17 10 15 16 mp2an 2 𝑜 + 𝑜 1 𝑜 2 𝑜 ⊔︀ 1 𝑜
18 17 ensymi 2 𝑜 ⊔︀ 1 𝑜 2 𝑜 + 𝑜 1 𝑜
19 oa1suc 2 𝑜 On 2 𝑜 + 𝑜 1 𝑜 = suc 2 𝑜
20 10 19 ax-mp 2 𝑜 + 𝑜 1 𝑜 = suc 2 𝑜
21 df-3o 3 𝑜 = suc 2 𝑜
22 20 21 eqtr4i 2 𝑜 + 𝑜 1 𝑜 = 3 𝑜
23 18 22 breqtri 2 𝑜 ⊔︀ 1 𝑜 3 𝑜
24 domentr A B ⊔︀ C 2 𝑜 ⊔︀ 1 𝑜 2 𝑜 ⊔︀ 1 𝑜 3 𝑜 A B ⊔︀ C 3 𝑜
25 14 23 24 mp2an A B ⊔︀ C 3 𝑜
26 domtr A B C A B ⊔︀ C A B ⊔︀ C 3 𝑜 A B C 3 𝑜
27 5 25 26 mp2an A B C 3 𝑜
28 1 27 eqbrtri A B C 3 𝑜