Metamath Proof Explorer

Theorem tr3dom

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

Ref Expression
Assertion tr3dom ⊢ABC≼3𝑜

Proof

Step Hyp Ref Expression
1 df-tp ⊢ABC=AB∪C
2 prex ⊢AB∈V
3 snex ⊢C∈V
4 undjudom ⊢AB∈V∧C∈V→AB∪C≼AB⊔︀C
5 2 3 4 mp2an ⊢AB∪C≼AB⊔︀C
6 pr2dom ⊢AB≼2𝑜
7 djudom1 ⊢AB≼2𝑜∧C∈V→AB⊔︀C≼2𝑜⊔︀C
8 6 3 7 mp2an ⊢AB⊔︀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 ⊢AB⊔︀C≼2𝑜⊔︀C∧2𝑜⊔︀C≼2𝑜⊔︀1𝑜→AB⊔︀C≼2𝑜⊔︀1𝑜
14 8 12 13 mp2an ⊢AB⊔︀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 ⊢AB⊔︀C≼2𝑜⊔︀1𝑜∧2𝑜⊔︀1𝑜≈3𝑜→AB⊔︀C≼3𝑜
25 14 23 24 mp2an ⊢AB⊔︀C≼3𝑜
26 domtr ⊢AB∪C≼AB⊔︀C∧AB⊔︀C≼3𝑜→AB∪C≼3𝑜
27 5 25 26 mp2an ⊢AB∪C≼3𝑜
28 1 27 eqbrtri ⊢ABC≼3𝑜