Theorem pr2dom

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

	Ref	Expression
Assertion	pr2dom	|- { A , B } ~<_ 2o

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		snex	|- { A } e. _V
3		snex	|- { B } e. _V
4		undjudom	|- ( ( { A } e. _V /\ { B } e. _V ) -> ( { A } u. { B } ) ~<_ ( { A } |_| { B } ) )
5	2 3 4	mp2an	|- ( { A } u. { B } ) ~<_ ( { A } |_| { B } )
6		sn1dom	|- { A } ~<_ 1o
7		djudom1	|- ( ( { A } ~<_ 1o /\ { B } e. _V ) -> ( { A } |_| { B } ) ~<_ ( 1o |_| { B } ) )
8	6 3 7	mp2an	|- ( { A } |_| { B } ) ~<_ ( 1o |_| { B } )
9		sn1dom	|- { B } ~<_ 1o
10		1on	|- 1o e. On
11		djudom2	|- ( ( { B } ~<_ 1o /\ 1o e. On ) -> ( 1o |_| { B } ) ~<_ ( 1o |_| 1o ) )
12	9 10 11	mp2an	|- ( 1o |_| { B } ) ~<_ ( 1o |_| 1o )
13		domtr	|- ( ( ( { A } |_| { B } ) ~<_ ( 1o |_| { B } ) /\ ( 1o |_| { B } ) ~<_ ( 1o |_| 1o ) ) -> ( { A } |_| { B } ) ~<_ ( 1o |_| 1o ) )
14	8 12 13	mp2an	|- ( { A } |_| { B } ) ~<_ ( 1o |_| 1o )
15		dju1p1e2	|- ( 1o |_| 1o ) ~~ 2o
16		domentr	|- ( ( ( { A } |_| { B } ) ~<_ ( 1o |_| 1o ) /\ ( 1o |_| 1o ) ~~ 2o ) -> ( { A } |_| { B } ) ~<_ 2o )
17	14 15 16	mp2an	|- ( { A } |_| { B } ) ~<_ 2o
18		domtr	|- ( ( ( { A } u. { B } ) ~<_ ( { A } |_| { B } ) /\ ( { A } |_| { B } ) ~<_ 2o ) -> ( { A } u. { B } ) ~<_ 2o )
19	5 17 18	mp2an	|- ( { A } u. { B } ) ~<_ 2o
20	1 19	eqbrtri	|- { A , B } ~<_ 2o