scottex

Description: Scott's trick collects all sets that have a certain property and are of the smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of Jech p. 72, is a set. (Contributed by NM, 13-Oct-2003)

		Ref	Expression
	Assertion	scottex	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		eleq1	$⊢ A = \emptyset \to (A \in V \leftrightarrow \emptyset \in V)$
3	1 2	mpbiri	$⊢ A = \emptyset \to A \in V$
4		rabexg	$⊢ A \in V \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
5	3 4	syl	$⊢ A = \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
6		neq0	$⊢ \neg A = \emptyset \leftrightarrow \exists y y \in A$
7		nfra1	$⊢ Ⅎ y \forall y \in A rank (x) \subseteq rank (y)$
8		nfcv	$⊢ \underline{Ⅎ} y A$
9	7 8	nfrabw	$⊢ \underline{Ⅎ} y \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\}$
10	9	nfel1	$⊢ Ⅎ y \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
11		rsp	$⊢ \forall y \in A rank (x) \subseteq rank (y) \to (y \in A \to rank (x) \subseteq rank (y))$
12	11	com12	$⊢ y \in A \to (\forall y \in A rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
13	12	ralrimivw	$⊢ y \in A \to \forall x \in A (\forall y \in A rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
14		ss2rab	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \subseteq \{x \in A \| rank (x) \subseteq rank (y)\} \leftrightarrow \forall x \in A (\forall y \in A rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
15	13 14	sylibr	$⊢ y \in A \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \subseteq \{x \in A \| rank (x) \subseteq rank (y)\}$
16		rankon	$⊢ rank (y) \in On$
17		fveq2	$⊢ x = w \to rank (x) = rank (w)$
18	17	sseq1d	$⊢ x = w \to (rank (x) \subseteq rank (y) \leftrightarrow rank (w) \subseteq rank (y))$
19	18	elrab	$⊢ w \in \{x \in A \| rank (x) \subseteq rank (y)\} \leftrightarrow (w \in A \land rank (w) \subseteq rank (y))$
20	19	simprbi	$⊢ w \in \{x \in A \| rank (x) \subseteq rank (y)\} \to rank (w) \subseteq rank (y)$
21	20	rgen	$⊢ \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq rank (y)$
22		sseq2	$⊢ z = rank (y) \to (rank (w) \subseteq z \leftrightarrow rank (w) \subseteq rank (y))$
23	22	ralbidv	$⊢ z = rank (y) \to (\forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq z \leftrightarrow \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq rank (y))$
24	23	rspcev	$⊢ (rank (y) \in On \land \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq rank (y)) \to \exists z \in On \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq z$
25	16 21 24	mp2an	$⊢ \exists z \in On \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq z$
26		bndrank	$⊢ \exists z \in On \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq z \to \{x \in A \| rank (x) \subseteq rank (y)\} \in V$
27	25 26	ax-mp	$⊢ \{x \in A \| rank (x) \subseteq rank (y)\} \in V$
28	27	ssex	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \subseteq \{x \in A \| rank (x) \subseteq rank (y)\} \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
29	15 28	syl	$⊢ y \in A \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
30	10 29	exlimi	$⊢ \exists y y \in A \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
31	6 30	sylbi	$⊢ \neg A = \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
32	5 31	pm2.61i	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$

Metamath Proof Explorer

Theorem scottex

Proof