Metamath Proof Explorer

Theorem ordsssuc2

Description: An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005) (Proof shortened by Andrew Salmon, 12-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		elong	$⊢ A \in V \to (A \in On \leftrightarrow Ord A)$
2	1	biimprd	$⊢ A \in V \to (Ord A \to A \in On)$
3	2	anim1d	$⊢ A \in V \to ((Ord A \land B \in On) \to (A \in On \land B \in On))$
4		onsssuc	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow A \in suc B)$
5	3 4	syl6	$⊢ A \in V \to ((Ord A \land B \in On) \to (A \subseteq B \leftrightarrow A \in suc B))$
6		annim	$⊢ (B \in On \land \neg A \in V) \leftrightarrow \neg (B \in On \to A \in V)$
7		ssexg	$⊢ (A \subseteq B \land B \in On) \to A \in V$
8	7	ex	$⊢ A \subseteq B \to (B \in On \to A \in V)$
9		elex	$⊢ A \in suc B \to A \in V$
10	9	a1d	$⊢ A \in suc B \to (B \in On \to A \in V)$
11	8 10	pm5.21ni	$⊢ \neg (B \in On \to A \in V) \to (A \subseteq B \leftrightarrow A \in suc B)$
12	6 11	sylbi	$⊢ (B \in On \land \neg A \in V) \to (A \subseteq B \leftrightarrow A \in suc B)$
13	12	expcom	$⊢ \neg A \in V \to (B \in On \to (A \subseteq B \leftrightarrow A \in suc B))$
14	13	adantld	$⊢ \neg A \in V \to ((Ord A \land B \in On) \to (A \subseteq B \leftrightarrow A \in suc B))$
15	5 14	pm2.61i	$⊢ (Ord A \land B \in On) \to (A \subseteq B \leftrightarrow A \in suc B)$