onnminsb

Description: An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ps is the wff resulting from the substitution of A for x in wff ph . (Contributed by NM, 9-Nov-2003)

		Ref	Expression
	Hypothesis	onnminsb.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	Assertion	onnminsb	$⊢ A \in On \to (A \in ⋂ \{x \in On \| φ\} \to \neg ψ)$

Proof

Step	Hyp	Ref	Expression
1		onnminsb.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2	1	elrab	$⊢ A \in \{x \in On \| φ\} \leftrightarrow (A \in On \land ψ)$
3		ssrab2	$⊢ \{x \in On \| φ\} \subseteq On$
4		onnmin	$⊢ (\{x \in On \| φ\} \subseteq On \land A \in \{x \in On \| φ\}) \to \neg A \in ⋂ \{x \in On \| φ\}$
5	3 4	mpan	$⊢ A \in \{x \in On \| φ\} \to \neg A \in ⋂ \{x \in On \| φ\}$
6	2 5	sylbir	$⊢ (A \in On \land ψ) \to \neg A \in ⋂ \{x \in On \| φ\}$
7	6	ex	$⊢ A \in On \to (ψ \to \neg A \in ⋂ \{x \in On \| φ\})$
8	7	con2d	$⊢ A \in On \to (A \in ⋂ \{x \in On \| φ\} \to \neg ψ)$

Metamath Proof Explorer

Theorem onnminsb

Proof