Theorem 1oequni2o

Description: The ordinal number 1o is the predecessor of the ordinal number 2o . (Contributed by ML, 19-Oct-2020)

	Ref	Expression
Assertion	1oequni2o	⊢ 1o = ∪ 2o

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2		2on	⊢ 2o ∈ On
3		2on0	⊢ 2o ≠ ∅
4		2onn	⊢ 2o ∈ ω
5		nnlim	⊢ ( 2o ∈ ω → ¬ Lim 2o )
6	4 5	ax-mp	⊢ ¬ Lim 2o
7		onsucuni3	⊢ ( ( 2o ∈ On ∧ 2o ≠ ∅ ∧ ¬ Lim 2o ) → 2o = suc ∪ 2o )
8	2 3 6 7	mp3an	⊢ 2o = suc ∪ 2o
9	1 8	eqtr3i	⊢ suc 1o = suc ∪ 2o
10		1on	⊢ 1o ∈ On
11		onuni	⊢ ( 2o ∈ On → ∪ 2o ∈ On )
12	2 11	ax-mp	⊢ ∪ 2o ∈ On
13		suc11	⊢ ( ( 1o ∈ On ∧ ∪ 2o ∈ On ) → ( suc 1o = suc ∪ 2o ↔ 1o = ∪ 2o ) )
14	10 12 13	mp2an	⊢ ( suc 1o = suc ∪ 2o ↔ 1o = ∪ 2o )
15	9 14	mpbi	⊢ 1o = ∪ 2o