Metamath Proof Explorer

Theorem onmindif

Description: When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003)

		Ref	Expression
	Assertion	onmindif	$⊢ (A \subseteq On \land B \in On) \to B \in ⋂ (A ∖ suc B)$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (A ∖ suc B) \leftrightarrow (x \in A \land \neg x \in suc B)$
2		ssel2	$⊢ (A \subseteq On \land x \in A) \to x \in On$
3		ontri1	$⊢ (x \in On \land B \in On) \to (x \subseteq B \leftrightarrow \neg B \in x)$
4		onsssuc	$⊢ (x \in On \land B \in On) \to (x \subseteq B \leftrightarrow x \in suc B)$
5	3 4	bitr3d	$⊢ (x \in On \land B \in On) \to (\neg B \in x \leftrightarrow x \in suc B)$
6	5	con1bid	$⊢ (x \in On \land B \in On) \to (\neg x \in suc B \leftrightarrow B \in x)$
7	2 6	sylan	$⊢ ((A \subseteq On \land x \in A) \land B \in On) \to (\neg x \in suc B \leftrightarrow B \in x)$
8	7	biimpd	$⊢ ((A \subseteq On \land x \in A) \land B \in On) \to (\neg x \in suc B \to B \in x)$
9	8	exp31	$⊢ A \subseteq On \to (x \in A \to (B \in On \to (\neg x \in suc B \to B \in x)))$
10	9	com23	$⊢ A \subseteq On \to (B \in On \to (x \in A \to (\neg x \in suc B \to B \in x)))$
11	10	imp4b	$⊢ (A \subseteq On \land B \in On) \to ((x \in A \land \neg x \in suc B) \to B \in x)$
12	1 11	biimtrid	$⊢ (A \subseteq On \land B \in On) \to (x \in (A ∖ suc B) \to B \in x)$
13	12	ralrimiv	$⊢ (A \subseteq On \land B \in On) \to \forall x \in (A ∖ suc B) B \in x$
14		elintg	$⊢ B \in On \to (B \in ⋂ (A ∖ suc B) \leftrightarrow \forall x \in (A ∖ suc B) B \in x)$
15	14	adantl	$⊢ (A \subseteq On \land B \in On) \to (B \in ⋂ (A ∖ suc B) \leftrightarrow \forall x \in (A ∖ suc B) B \in x)$
16	13 15	mpbird	$⊢ (A \subseteq On \land B \in On) \to B \in ⋂ (A ∖ suc B)$