scott0

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, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. A is empty). (Contributed by NM, 15-Oct-2003)

		Ref	Expression
	Assertion	scott0	$⊢ A = \emptyset \leftrightarrow \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		rabeq	$⊢ A = \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} = \{x \in \emptyset \| \forall y \in A rank (x) \subseteq rank (y)\}$
2		rab0	$⊢ \{x \in \emptyset \| \forall y \in A rank (x) \subseteq rank (y)\} = \emptyset$
3	1 2	eqtrdi	$⊢ A = \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} = \emptyset$
4		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
5		nfre1	$⊢ Ⅎ x \exists x \in A rank (x) = rank (x)$
6		eqid	$⊢ rank (x) = rank (x)$
7		rspe	$⊢ (x \in A \land rank (x) = rank (x)) \to \exists x \in A rank (x) = rank (x)$
8	6 7	mpan2	$⊢ x \in A \to \exists x \in A rank (x) = rank (x)$
9	5 8	exlimi	$⊢ \exists x x \in A \to \exists x \in A rank (x) = rank (x)$
10	4 9	sylbi	$⊢ A \neq \emptyset \to \exists x \in A rank (x) = rank (x)$
11		fvex	$⊢ rank (x) \in V$
12		eqeq1	$⊢ y = rank (x) \to (y = rank (x) \leftrightarrow rank (x) = rank (x))$
13	12	anbi2d	$⊢ y = rank (x) \to ((x \in A \land y = rank (x)) \leftrightarrow (x \in A \land rank (x) = rank (x)))$
14	11 13	spcev	$⊢ (x \in A \land rank (x) = rank (x)) \to \exists y (x \in A \land y = rank (x))$
15	14	eximi	$⊢ \exists x (x \in A \land rank (x) = rank (x)) \to \exists x \exists y (x \in A \land y = rank (x))$
16		excom	$⊢ \exists y \exists x (x \in A \land y = rank (x)) \leftrightarrow \exists x \exists y (x \in A \land y = rank (x))$
17	15 16	sylibr	$⊢ \exists x (x \in A \land rank (x) = rank (x)) \to \exists y \exists x (x \in A \land y = rank (x))$
18		df-rex	$⊢ \exists x \in A rank (x) = rank (x) \leftrightarrow \exists x (x \in A \land rank (x) = rank (x))$
19		df-rex	$⊢ \exists x \in A y = rank (x) \leftrightarrow \exists x (x \in A \land y = rank (x))$
20	19	exbii	$⊢ \exists y \exists x \in A y = rank (x) \leftrightarrow \exists y \exists x (x \in A \land y = rank (x))$
21	17 18 20	3imtr4i	$⊢ \exists x \in A rank (x) = rank (x) \to \exists y \exists x \in A y = rank (x)$
22	10 21	syl	$⊢ A \neq \emptyset \to \exists y \exists x \in A y = rank (x)$
23		abn0	$⊢ \{y \| \exists x \in A y = rank (x)\} \neq \emptyset \leftrightarrow \exists y \exists x \in A y = rank (x)$
24	22 23	sylibr	$⊢ A \neq \emptyset \to \{y \| \exists x \in A y = rank (x)\} \neq \emptyset$
25	11	dfiin2	$⊢ ⋂_{x \in A} rank (x) = ⋂ \{y \| \exists x \in A y = rank (x)\}$
26		rankon	$⊢ rank (x) \in On$
27		eleq1	$⊢ y = rank (x) \to (y \in On \leftrightarrow rank (x) \in On)$
28	26 27	mpbiri	$⊢ y = rank (x) \to y \in On$
29	28	rexlimivw	$⊢ \exists x \in A y = rank (x) \to y \in On$
30	29	abssi	$⊢ \{y \| \exists x \in A y = rank (x)\} \subseteq On$
31		onint	$⊢ (\{y \| \exists x \in A y = rank (x)\} \subseteq On \land \{y \| \exists x \in A y = rank (x)\} \neq \emptyset) \to ⋂ \{y \| \exists x \in A y = rank (x)\} \in \{y \| \exists x \in A y = rank (x)\}$
32	30 31	mpan	$⊢ \{y \| \exists x \in A y = rank (x)\} \neq \emptyset \to ⋂ \{y \| \exists x \in A y = rank (x)\} \in \{y \| \exists x \in A y = rank (x)\}$
33	25 32	eqeltrid	$⊢ \{y \| \exists x \in A y = rank (x)\} \neq \emptyset \to ⋂_{x \in A} rank (x) \in \{y \| \exists x \in A y = rank (x)\}$
34		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} rank (x)$
35	34	nfeq2	$⊢ Ⅎ x y = ⋂_{x \in A} rank (x)$
36		eqeq1	$⊢ y = ⋂_{x \in A} rank (x) \to (y = rank (x) \leftrightarrow ⋂_{x \in A} rank (x) = rank (x))$
37	35 36	rexbid	$⊢ y = ⋂_{x \in A} rank (x) \to (\exists x \in A y = rank (x) \leftrightarrow \exists x \in A ⋂_{x \in A} rank (x) = rank (x))$
38	37	elabg	$⊢ ⋂_{x \in A} rank (x) \in \{y \| \exists x \in A y = rank (x)\} \to (⋂_{x \in A} rank (x) \in \{y \| \exists x \in A y = rank (x)\} \leftrightarrow \exists x \in A ⋂_{x \in A} rank (x) = rank (x))$
39	38	ibi	$⊢ ⋂_{x \in A} rank (x) \in \{y \| \exists x \in A y = rank (x)\} \to \exists x \in A ⋂_{x \in A} rank (x) = rank (x)$
40		ssid	$⊢ rank (y) \subseteq rank (y)$
41		fveq2	$⊢ x = y \to rank (x) = rank (y)$
42	41	sseq1d	$⊢ x = y \to (rank (x) \subseteq rank (y) \leftrightarrow rank (y) \subseteq rank (y))$
43	42	rspcev	$⊢ (y \in A \land rank (y) \subseteq rank (y)) \to \exists x \in A rank (x) \subseteq rank (y)$
44	40 43	mpan2	$⊢ y \in A \to \exists x \in A rank (x) \subseteq rank (y)$
45		iinss	$⊢ \exists x \in A rank (x) \subseteq rank (y) \to ⋂_{x \in A} rank (x) \subseteq rank (y)$
46	44 45	syl	$⊢ y \in A \to ⋂_{x \in A} rank (x) \subseteq rank (y)$
47		sseq1	$⊢ ⋂_{x \in A} rank (x) = rank (x) \to (⋂_{x \in A} rank (x) \subseteq rank (y) \leftrightarrow rank (x) \subseteq rank (y))$
48	46 47	syl5ib	$⊢ ⋂_{x \in A} rank (x) = rank (x) \to (y \in A \to rank (x) \subseteq rank (y))$
49	48	ralrimiv	$⊢ ⋂_{x \in A} rank (x) = rank (x) \to \forall y \in A rank (x) \subseteq rank (y)$
50	49	reximi	$⊢ \exists x \in A ⋂_{x \in A} rank (x) = rank (x) \to \exists x \in A \forall y \in A rank (x) \subseteq rank (y)$
51	24 33 39 50	4syl	$⊢ A \neq \emptyset \to \exists x \in A \forall y \in A rank (x) \subseteq rank (y)$
52		rabn0	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \neq \emptyset \leftrightarrow \exists x \in A \forall y \in A rank (x) \subseteq rank (y)$
53	51 52	sylibr	$⊢ A \neq \emptyset \to \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} \neq \emptyset$
54	53	necon4i	$⊢ \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} = \emptyset \to A = \emptyset$
55	3 54	impbii	$⊢ A = \emptyset \leftrightarrow \{x \in A \| \forall y \in A rank (x) \subseteq rank (y)\} = \emptyset$

Metamath Proof Explorer

Theorem scott0

Proof