# Metamath Proof Explorer

## Theorem 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 \left({\phi }↔{\psi }\right)$
Assertion onnminsb ${⊢}{A}\in \mathrm{On}\to \left({A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}\to ¬{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 onnminsb.1 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
2 1 elrab ${⊢}{A}\in \left\{{x}\in \mathrm{On}|{\phi }\right\}↔\left({A}\in \mathrm{On}\wedge {\psi }\right)$
3 ssrab2 ${⊢}\left\{{x}\in \mathrm{On}|{\phi }\right\}\subseteq \mathrm{On}$
4 onnmin ${⊢}\left(\left\{{x}\in \mathrm{On}|{\phi }\right\}\subseteq \mathrm{On}\wedge {A}\in \left\{{x}\in \mathrm{On}|{\phi }\right\}\right)\to ¬{A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}$
5 3 4 mpan ${⊢}{A}\in \left\{{x}\in \mathrm{On}|{\phi }\right\}\to ¬{A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}$
6 2 5 sylbir ${⊢}\left({A}\in \mathrm{On}\wedge {\psi }\right)\to ¬{A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}$
7 6 ex ${⊢}{A}\in \mathrm{On}\to \left({\psi }\to ¬{A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}\right)$
8 7 con2d ${⊢}{A}\in \mathrm{On}\to \left({A}\in \bigcap \left\{{x}\in \mathrm{On}|{\phi }\right\}\to ¬{\psi }\right)$