Theorem tr3dom

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

	Ref	Expression
Assertion	tr3dom	⊢ { 𝐴 , 𝐵 , 𝐶 } ≼ 3o

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
2		prex	⊢ { 𝐴 , 𝐵 } ∈ V
3		snex	⊢ { 𝐶 } ∈ V
4		undjudom	⊢ ( ( { 𝐴 , 𝐵 } ∈ V ∧ { 𝐶 } ∈ V ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ≼ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) )
5	2 3 4	mp2an	⊢ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ≼ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } )
6		pr2dom	⊢ { 𝐴 , 𝐵 } ≼ 2o
7		djudom1	⊢ ( ( { 𝐴 , 𝐵 } ≼ 2o ∧ { 𝐶 } ∈ V ) → ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ { 𝐶 } ) )
8	6 3 7	mp2an	⊢ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ { 𝐶 } )
9		sn1dom	⊢ { 𝐶 } ≼ 1o
10		2on	⊢ 2o ∈ On
11		djudom2	⊢ ( ( { 𝐶 } ≼ 1o ∧ 2o ∈ On ) → ( 2o ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o ) )
12	9 10 11	mp2an	⊢ ( 2o ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o )
13		domtr	⊢ ( ( ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ { 𝐶 } ) ∧ ( 2o ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o ) ) → ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o ) )
14	8 12 13	mp2an	⊢ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o )
15		1on	⊢ 1o ∈ On
16		onadju	⊢ ( ( 2o ∈ On ∧ 1o ∈ On ) → ( 2o +o 1o ) ≈ ( 2o ⊔ 1o ) )
17	10 15 16	mp2an	⊢ ( 2o +o 1o ) ≈ ( 2o ⊔ 1o )
18	17	ensymi	⊢ ( 2o ⊔ 1o ) ≈ ( 2o +o 1o )
19		oa1suc	⊢ ( 2o ∈ On → ( 2o +o 1o ) = suc 2o )
20	10 19	ax-mp	⊢ ( 2o +o 1o ) = suc 2o
21		df-3o	⊢ 3o = suc 2o
22	20 21	eqtr4i	⊢ ( 2o +o 1o ) = 3o
23	18 22	breqtri	⊢ ( 2o ⊔ 1o ) ≈ 3o
24		domentr	⊢ ( ( ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ ( 2o ⊔ 1o ) ∧ ( 2o ⊔ 1o ) ≈ 3o ) → ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ 3o )
25	14 23 24	mp2an	⊢ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ 3o
26		domtr	⊢ ( ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ≼ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ∧ ( { 𝐴 , 𝐵 } ⊔ { 𝐶 } ) ≼ 3o ) → ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ≼ 3o )
27	5 25 26	mp2an	⊢ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ≼ 3o
28	1 27	eqbrtri	⊢ { 𝐴 , 𝐵 , 𝐶 } ≼ 3o