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 𝑜