Metamath Proof Explorer

Theorem onsucssi

Description: A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of TakeutiZaring p. 42 and its converse. (Contributed by NM, 16-Sep-1995)

	Ref	Expression
Hypotheses	onssi.1	$⊢ A \in On$
	onsucssi.2	$⊢ B \in On$
Assertion	onsucssi	$⊢ A \in B \leftrightarrow suc A \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		onssi.1	$⊢ A \in On$
2		onsucssi.2	$⊢ B \in On$
3	2	onordi	$⊢ Ord B$
4		ordelsuc	$⊢ (A \in On \land Ord B) \to (A \in B \leftrightarrow suc A \subseteq B)$
5	1 3 4	mp2an	$⊢ A \in B \leftrightarrow suc A \subseteq B$