Metamath Proof Explorer

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 A \land A \subseteq \{x \in On \| \neg Lim x\}) \to A \subseteq ω$

Proof

Step	Hyp	Ref	Expression
1		limom	$⊢ Lim ω$
2		ssel	$⊢ A \subseteq \{x \in On \| \neg Lim x\} \to (ω \in A \to ω \in \{x \in On \| \neg Lim x\})$
3		limeq	$⊢ x = ω \to (Lim x \leftrightarrow Lim ω)$
4	3	notbid	$⊢ x = ω \to (\neg Lim x \leftrightarrow \neg Lim ω)$
5	4	elrab	$⊢ ω \in \{x \in On \| \neg Lim x\} \leftrightarrow (ω \in On \land \neg Lim ω)$
6	5	simprbi	$⊢ ω \in \{x \in On \| \neg Lim x\} \to \neg Lim ω$
7	2 6	syl6	$⊢ A \subseteq \{x \in On \| \neg Lim x\} \to (ω \in A \to \neg Lim ω)$
8	1 7	mt2i	$⊢ A \subseteq \{x \in On \| \neg Lim x\} \to \neg ω \in A$
9	8	adantl	$⊢ (Ord A \land A \subseteq \{x \in On \| \neg Lim x\}) \to \neg ω \in A$
10		ordom	$⊢ Ord ω$
11		ordtri1	$⊢ (Ord A \land Ord ω) \to (A \subseteq ω \leftrightarrow \neg ω \in A)$
12	10 11	mpan2	$⊢ Ord A \to (A \subseteq ω \leftrightarrow \neg ω \in A)$
13	12	adantr	$⊢ (Ord A \land A \subseteq \{x \in On \| \neg Lim x\}) \to (A \subseteq ω \leftrightarrow \neg ω \in A)$
14	9 13	mpbird	$⊢ (Ord A \land A \subseteq \{x \in On \| \neg Lim x\}) \to A \subseteq ω$