Theorem pr2dom

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

	Ref	Expression
Assertion	pr2dom	⊢ { 𝐴 , 𝐵 } ≼ 2o

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		snex	⊢ { 𝐴 } ∈ V
3		snex	⊢ { 𝐵 } ∈ V
4		undjudom	⊢ ( ( { 𝐴 } ∈ V ∧ { 𝐵 } ∈ V ) → ( { 𝐴 } ∪ { 𝐵 } ) ≼ ( { 𝐴 } ⊔ { 𝐵 } ) )
5	2 3 4	mp2an	⊢ ( { 𝐴 } ∪ { 𝐵 } ) ≼ ( { 𝐴 } ⊔ { 𝐵 } )
6		sn1dom	⊢ { 𝐴 } ≼ 1o
7		djudom1	⊢ ( ( { 𝐴 } ≼ 1o ∧ { 𝐵 } ∈ V ) → ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ { 𝐵 } ) )
8	6 3 7	mp2an	⊢ ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ { 𝐵 } )
9		sn1dom	⊢ { 𝐵 } ≼ 1o
10		1on	⊢ 1o ∈ On
11		djudom2	⊢ ( ( { 𝐵 } ≼ 1o ∧ 1o ∈ On ) → ( 1o ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o ) )
12	9 10 11	mp2an	⊢ ( 1o ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o )
13		domtr	⊢ ( ( ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ { 𝐵 } ) ∧ ( 1o ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o ) ) → ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o ) )
14	8 12 13	mp2an	⊢ ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o )
15		dju1p1e2	⊢ ( 1o ⊔ 1o ) ≈ 2o
16		domentr	⊢ ( ( ( { 𝐴 } ⊔ { 𝐵 } ) ≼ ( 1o ⊔ 1o ) ∧ ( 1o ⊔ 1o ) ≈ 2o ) → ( { 𝐴 } ⊔ { 𝐵 } ) ≼ 2o )
17	14 15 16	mp2an	⊢ ( { 𝐴 } ⊔ { 𝐵 } ) ≼ 2o
18		domtr	⊢ ( ( ( { 𝐴 } ∪ { 𝐵 } ) ≼ ( { 𝐴 } ⊔ { 𝐵 } ) ∧ ( { 𝐴 } ⊔ { 𝐵 } ) ≼ 2o ) → ( { 𝐴 } ∪ { 𝐵 } ) ≼ 2o )
19	5 17 18	mp2an	⊢ ( { 𝐴 } ∪ { 𝐵 } ) ≼ 2o
20	1 19	eqbrtri	⊢ { 𝐴 , 𝐵 } ≼ 2o