Theorem scott0s

Description: Theorem scheme version of scott0 . The collection of all x of minimum rank such that ph ( x ) is true, is not empty iff there is an x such that ph ( x ) holds. (Contributed by NM, 13-Oct-2003)

	Ref	Expression
Assertion	scott0s	$$⊢\exists x\phi \leftrightarrow \left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		abn0	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \exists x\phi$$
2		scott0	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \left\{z\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\varnothing$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}z\left\{x|\phi \right\}$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
5		nfv	$$⊢Ⅎx\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)$$
6	4 5	nfralw	$$⊢Ⅎx\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)$$
7		nfv	$$⊢Ⅎz\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)$$
8		fveq2	$$⊢z=x\to \mathrm{rank}\left(z\right)=\mathrm{rank}\left(x\right)$$
9	8	sseq1d	$$⊢z=x\to \left(\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
10	9	ralbidv	$$⊢z=x\to \left(\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
11	3 4 6 7 10	cbvrabw	$$⊢\left\{z\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{x\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$
12		df-rab	$$⊢\left\{x\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{x|\left(x\in \left\{x|\phi \right\}\wedge \forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right\}$$
13		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
14		df-ral	$$⊢\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
15		df-sbc	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y\in \left\{x|\phi \right\}$$
16	15	imbi1i	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(y\in \left\{x|\phi \right\}\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
17	16	albii	$$⊢\forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
18	14 17	bitr4i	$$⊢\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
19	13 18	anbi12i	$$⊢\left(x\in \left\{x|\phi \right\}\wedge \forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
20	19	abbii	$$⊢\left\{x|\left(x\in \left\{x|\phi \right\}\wedge \forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right\}=\left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
21	11 12 20	3eqtri	$$⊢\left\{z\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
22	21	eqeq1i	$$⊢\left\{z\in \left\{x|\phi \right\}|\forall y\in \left\{x|\phi \right\}\mathrm{rank}\left(z\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\varnothing \leftrightarrow \left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}=\varnothing$$
23	2 22	bitri	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}=\varnothing$$
24	23	necon3bii	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\ne \varnothing$$
25	1 24	bitr3i	$$⊢\exists x\phi \leftrightarrow \left\{x|\left(\phi \wedge \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\ne \varnothing$$