Theorem ordtoplem

Description: Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015)

	Ref	Expression
Hypothesis	ordtoplem.1	⊢ ( ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆 )
Assertion	ordtoplem	⊢ ( Ord 𝐴 → ( 𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtoplem.1	⊢ ( ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆 )
2		df-ne	⊢ ( 𝐴 ≠ ∪ 𝐴 ↔ ¬ 𝐴 = ∪ 𝐴 )
3		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4		unon	⊢ ∪ On = On
5	4	eqcomi	⊢ On = ∪ On
6		id	⊢ ( 𝐴 = On → 𝐴 = On )
7		unieq	⊢ ( 𝐴 = On → ∪ 𝐴 = ∪ On )
8	5 6 7	3eqtr4a	⊢ ( 𝐴 = On → 𝐴 = ∪ 𝐴 )
9	8	orim2i	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( 𝐴 ∈ On ∨ 𝐴 = ∪ 𝐴 ) )
10	3 9	sylbi	⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = ∪ 𝐴 ) )
11	10	orcomd	⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 ∈ On ) )
12	11	ord	⊢ ( Ord 𝐴 → ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 ∈ On ) )
13		orduniorsuc	⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
14	13	ord	⊢ ( Ord 𝐴 → ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 ) )
15		onuni	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
16		eleq1a	⊢ ( suc ∪ 𝐴 ∈ 𝑆 → ( 𝐴 = suc ∪ 𝐴 → 𝐴 ∈ 𝑆 ) )
17	15 1 16	3syl	⊢ ( 𝐴 ∈ On → ( 𝐴 = suc ∪ 𝐴 → 𝐴 ∈ 𝑆 ) )
18	12 14 17	syl6c	⊢ ( Ord 𝐴 → ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 ∈ 𝑆 ) )
19	2 18	syl5bi	⊢ ( Ord 𝐴 → ( 𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆 ) )