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	adantr	$⊢ (y \in A \land x \in A) \to (\forall y \in A rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
14	13	ss2rabdv	$⊢ 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)\}$
15		rankon	$⊢ rank (y) \in On$
16		fveq2	$⊢ x = w \to rank (x) = rank (w)$
17	16	sseq1d	$⊢ x = w \to (rank (x) \subseteq rank (y) \leftrightarrow rank (w) \subseteq rank (y))$
18	17	elrab	$⊢ w \in \{x \in A \| rank (x) \subseteq rank (y)\} \leftrightarrow (w \in A \land rank (w) \subseteq rank (y))$
19	18	simprbi	$⊢ w \in \{x \in A \| rank (x) \subseteq rank (y)\} \to rank (w) \subseteq rank (y)$
20	19	rgen	$⊢ \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq rank (y)$
21		sseq2	$⊢ z = rank (y) \to (rank (w) \subseteq z \leftrightarrow rank (w) \subseteq rank (y))$
22	21	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))$
23	22	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$
24	15 20 23	mp2an	$⊢ \exists z \in On \forall w \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (w) \subseteq z$
25		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$
26	24 25	ax-mp	$⊢ \{x \in A \| rank (x) \subseteq rank (y)\} \in V$
27	26	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$
28	14 27	syl	$⊢ y \in A \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
29	10 28	exlimi	$⊢ \exists y y \in A \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
30	6 29	sylbi	$⊢ \neg A = \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$
31	5 30	pm2.61i	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \in V$

Metamath Proof Explorer

Theorem scottex

Proof