onsucmin

Description: The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003)

		Ref	Expression
	Assertion	onsucmin	$⊢ A \in On \to suc A = ⋂ \{x \in On \| A \in x\}$

Step	Hyp	Ref	Expression
1		eloni	$⊢ x \in On \to Ord x$
2		ordelsuc	$⊢ (A \in On \land Ord x) \to (A \in x \leftrightarrow suc A \subseteq x)$
3	1 2	sylan2	$⊢ (A \in On \land x \in On) \to (A \in x \leftrightarrow suc A \subseteq x)$
4	3	rabbidva	$⊢ A \in On \to \{x \in On \| A \in x\} = \{x \in On \| suc A \subseteq x\}$
5	4	inteqd	$⊢ A \in On \to ⋂ \{x \in On \| A \in x\} = ⋂ \{x \in On \| suc A \subseteq x\}$
6		sucelon	$⊢ A \in On \leftrightarrow suc A \in On$
7		intmin	$⊢ suc A \in On \to ⋂ \{x \in On \| suc A \subseteq x\} = suc A$
8	6 7	sylbi	$⊢ A \in On \to ⋂ \{x \in On \| suc A \subseteq x\} = suc A$
9	5 8	eqtr2d	$⊢ A \in On \to suc A = ⋂ \{x \in On \| A \in x\}$

Metamath Proof Explorer