Metamath Proof Explorer

Theorem ordelsuc

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

		Ref	Expression
	Assertion	ordelsuc	$⊢ (A \in C \land Ord B) \to (A \in B \leftrightarrow suc A \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		ordsucss	$⊢ Ord B \to (A \in B \to suc A \subseteq B)$
2	1	adantl	$⊢ (A \in C \land Ord B) \to (A \in B \to suc A \subseteq B)$
3		sucssel	$⊢ A \in C \to (suc A \subseteq B \to A \in B)$
4	3	adantr	$⊢ (A \in C \land Ord B) \to (suc A \subseteq B \to A \in B)$
5	2 4	impbid	$⊢ (A \in C \land Ord B) \to (A \in B \leftrightarrow suc A \subseteq B)$