scott0OLD

Description: Obsolete version of scott0b as of 19-Jul-2026. (Contributed by NM, 15-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	scott0OLD	$⊢ 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	imbitrid	$⊢ ⋂_{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 scott0OLD

Proof