Theorem ssnlim

Description: An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of TakeutiZaring p. 42. (Contributed by NM, 2-Nov-2004)

	Ref	Expression
Assertion	ssnlim	⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → 𝐴 ⊆ ω )

Proof

Step	Hyp	Ref	Expression
1		limom	⊢ Lim ω
2		ssel	⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ( ω ∈ 𝐴 → ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) )
3		limeq	⊢ ( 𝑥 = ω → ( Lim 𝑥 ↔ Lim ω ) )
4	3	notbid	⊢ ( 𝑥 = ω → ( ¬ Lim 𝑥 ↔ ¬ Lim ω ) )
5	4	elrab	⊢ ( ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ↔ ( ω ∈ On ∧ ¬ Lim ω ) )
6	5	simprbi	⊢ ( ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ¬ Lim ω )
7	2 6	syl6	⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ( ω ∈ 𝐴 → ¬ Lim ω ) )
8	1 7	mt2i	⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ¬ ω ∈ 𝐴 )
9	8	adantl	⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → ¬ ω ∈ 𝐴 )
10		ordom	⊢ Ord ω
11		ordtri1	⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
12	10 11	mpan2	⊢ ( Ord 𝐴 → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
13	12	adantr	⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
14	9 13	mpbird	⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → 𝐴 ⊆ ω )