Theorem onminesb

Description: If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of Suppes p. 228. (Contributed by NM, 29-Sep-2003)

	Ref	Expression
Assertion	onminesb	$$⊢\exists x\in \mathrm{On}\phi \to \underset{\dot{}}{[}\bigcap \left\{x\in \mathrm{On}|\phi \right\}/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		rabn0	$$⊢\left\{x\in \mathrm{On}|\phi \right\}\ne \varnothing \leftrightarrow \exists x\in \mathrm{On}\phi$$
2		ssrab2	$$⊢\left\{x\in \mathrm{On}|\phi \right\}\subseteq \mathrm{On}$$
3		onint	$$⊢\left(\left\{x\in \mathrm{On}|\phi \right\}\subseteq \mathrm{On}\wedge \left\{x\in \mathrm{On}|\phi \right\}\ne \varnothing \right)\to \bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \left\{x\in \mathrm{On}|\phi \right\}$$
4	2 3	mpan	$$⊢\left\{x\in \mathrm{On}|\phi \right\}\ne \varnothing \to \bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \left\{x\in \mathrm{On}|\phi \right\}$$
5	1 4	sylbir	$$⊢\exists x\in \mathrm{On}\phi \to \bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \left\{x\in \mathrm{On}|\phi \right\}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{On}$$
7	6	elrabsf	$$⊢\bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \left\{x\in \mathrm{On}|\phi \right\}\leftrightarrow \left(\bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \mathrm{On}\wedge \underset{\dot{}}{[}\bigcap \left\{x\in \mathrm{On}|\phi \right\}/x\underset{\dot{}}{]}\phi \right)$$
8	7	simprbi	$$⊢\bigcap \left\{x\in \mathrm{On}|\phi \right\}\in \left\{x\in \mathrm{On}|\phi \right\}\to \underset{\dot{}}{[}\bigcap \left\{x\in \mathrm{On}|\phi \right\}/x\underset{\dot{}}{]}\phi$$
9	5 8	syl	$$⊢\exists x\in \mathrm{On}\phi \to \underset{\dot{}}{[}\bigcap \left\{x\in \mathrm{On}|\phi \right\}/x\underset{\dot{}}{]}\phi$$