Metamath Proof Explorer

Theorem tsksuc

Description: If an element of a Tarski class is an ordinal number, its successor is an element of the class. JFM CLASSES2 th. 6 (partly). (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

		Ref	Expression
	Assertion	tsksuc	$⊢ (T \in Tarski \land A \in On \land A \in T) \to suc A \in T$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (T \in Tarski \land A \in On \land A \in T) \to T \in Tarski$
2		tskpw	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A \in T$
3	2	3adant2	$⊢ (T \in Tarski \land A \in On \land A \in T) \to 𝒫 A \in T$
4		eloni	$⊢ A \in On \to Ord A$
5	4	3ad2ant2	$⊢ (T \in Tarski \land A \in On \land A \in T) \to Ord A$
6		ordunisuc	$⊢ Ord A \to ⋃ suc A = A$
7		eqimss	$⊢ ⋃ suc A = A \to ⋃ suc A \subseteq A$
8	5 6 7	3syl	$⊢ (T \in Tarski \land A \in On \land A \in T) \to ⋃ suc A \subseteq A$
9		sspwuni	$⊢ suc A \subseteq 𝒫 A \leftrightarrow ⋃ suc A \subseteq A$
10	8 9	sylibr	$⊢ (T \in Tarski \land A \in On \land A \in T) \to suc A \subseteq 𝒫 A$
11		tskss	$⊢ (T \in Tarski \land 𝒫 A \in T \land suc A \subseteq 𝒫 A) \to suc A \in T$
12	1 3 10 11	syl3anc	$⊢ (T \in Tarski \land A \in On \land A \in T) \to suc A \in T$