Theorem tr3dom

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

	Ref	Expression
Assertion	tr3dom	|- { A , B , C } ~<_ 3o

Proof

Step	Hyp	Ref	Expression
1		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
2		prex	|- { A , B } e. _V
3		snex	|- { C } e. _V
4		undjudom	|- ( ( { A , B } e. _V /\ { C } e. _V ) -> ( { A , B } u. { C } ) ~<_ ( { A , B } |_| { C } ) )
5	2 3 4	mp2an	|- ( { A , B } u. { C } ) ~<_ ( { A , B } |_| { C } )
6		pr2dom	|- { A , B } ~<_ 2o
7		djudom1	|- ( ( { A , B } ~<_ 2o /\ { C } e. _V ) -> ( { A , B } |_| { C } ) ~<_ ( 2o |_| { C } ) )
8	6 3 7	mp2an	|- ( { A , B } |_| { C } ) ~<_ ( 2o |_| { C } )
9		sn1dom	|- { C } ~<_ 1o
10		2on	|- 2o e. On
11		djudom2	|- ( ( { C } ~<_ 1o /\ 2o e. On ) -> ( 2o |_| { C } ) ~<_ ( 2o |_| 1o ) )
12	9 10 11	mp2an	|- ( 2o |_| { C } ) ~<_ ( 2o |_| 1o )
13		domtr	|- ( ( ( { A , B } |_| { C } ) ~<_ ( 2o |_| { C } ) /\ ( 2o |_| { C } ) ~<_ ( 2o |_| 1o ) ) -> ( { A , B } |_| { C } ) ~<_ ( 2o |_| 1o ) )
14	8 12 13	mp2an	|- ( { A , B } |_| { C } ) ~<_ ( 2o |_| 1o )
15		1on	|- 1o e. On
16		onadju	|- ( ( 2o e. On /\ 1o e. 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 e. 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	|- ( ( ( { A , B } |_| { C } ) ~<_ ( 2o |_| 1o ) /\ ( 2o |_| 1o ) ~~ 3o ) -> ( { A , B } |_| { C } ) ~<_ 3o )
25	14 23 24	mp2an	|- ( { A , B } |_| { C } ) ~<_ 3o
26		domtr	|- ( ( ( { A , B } u. { C } ) ~<_ ( { A , B } |_| { C } ) /\ ( { A , B } |_| { C } ) ~<_ 3o ) -> ( { A , B } u. { C } ) ~<_ 3o )
27	5 25 26	mp2an	|- ( { A , B } u. { C } ) ~<_ 3o
28	1 27	eqbrtri	|- { A , B , C } ~<_ 3o