Metamath Proof Explorer

Theorem predon

Description: The predecessor of an ordinal under _E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011)

		Ref	Expression
	Assertion	predon	$⊢ A \in On \to Pred (E, On, A) = A$

Step	Hyp	Ref	Expression
1		predep	$⊢ A \in On \to Pred (E, On, A) = On \cap A$
2		onss	$⊢ A \in On \to A \subseteq On$
3		sseqin2	$⊢ A \subseteq On \leftrightarrow On \cap A = A$
4	2 3	sylib	$⊢ A \in On \to On \cap A = A$
5	1 4	eqtrd	$⊢ A \in On \to Pred (E, On, A) = A$