scott0b

Description: Applying Scott's trick yields the empty set iff it was applied to the empty set. (Contributed by NM, 15-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

		Ref	Expression
	Assertion	scott0b	$⊢ A = \emptyset \leftrightarrow Scott A = \emptyset$

Proof

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

Metamath Proof Explorer

Theorem scott0b

Proof