rankeq1o

Description: The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015)

		Ref	Expression
	Assertion	rankeq1o	$⊢ rank (A) = 1_{𝑜} \leftrightarrow A = \{\emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		1n0	$⊢ 1_{𝑜} \neq \emptyset$
2		neeq1	$⊢ rank (A) = 1_{𝑜} \to (rank (A) \neq \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
3	1 2	mpbiri	$⊢ rank (A) = 1_{𝑜} \to rank (A) \neq \emptyset$
4	3	neneqd	$⊢ rank (A) = 1_{𝑜} \to \neg rank (A) = \emptyset$
5		fvprc	$⊢ \neg A \in V \to rank (A) = \emptyset$
6	4 5	nsyl2	$⊢ rank (A) = 1_{𝑜} \to A \in V$
7		fveqeq2	$⊢ x = A \to (rank (x) = 1_{𝑜} \leftrightarrow rank (A) = 1_{𝑜})$
8		eqeq1	$⊢ x = A \to (x = 1_{𝑜} \leftrightarrow A = 1_{𝑜})$
9	7 8	imbi12d	$⊢ x = A \to ((rank (x) = 1_{𝑜} \to x = 1_{𝑜}) \leftrightarrow (rank (A) = 1_{𝑜} \to A = 1_{𝑜}))$
10		neeq1	$⊢ rank (x) = 1_{𝑜} \to (rank (x) \neq \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
11	1 10	mpbiri	$⊢ rank (x) = 1_{𝑜} \to rank (x) \neq \emptyset$
12		vex	$⊢ x \in V$
13	12	rankeq0	$⊢ x = \emptyset \leftrightarrow rank (x) = \emptyset$
14	13	necon3bii	$⊢ x \neq \emptyset \leftrightarrow rank (x) \neq \emptyset$
15	11 14	sylibr	$⊢ rank (x) = 1_{𝑜} \to x \neq \emptyset$
16	12	rankval	$⊢ rank (x) = ⋂ \{y \in On \| x \in R_{1} (suc y)\}$
17	16	eqeq1i	$⊢ rank (x) = 1_{𝑜} \leftrightarrow ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜}$
18		ssrab2	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \subseteq On$
19		elirr	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
20		1oex	$⊢ 1_{𝑜} \in V$
21		id	$⊢ V = 1_{𝑜} \to V = 1_{𝑜}$
22	20 21	eleqtrid	$⊢ V = 1_{𝑜} \to 1_{𝑜} \in 1_{𝑜}$
23	19 22	mto	$⊢ \neg V = 1_{𝑜}$
24		inteq	$⊢ \{y \in On \| x \in R_{1} (suc y)\} = \emptyset \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} = ⋂ \emptyset$
25		int0	$⊢ ⋂ \emptyset = V$
26	24 25	eqtrdi	$⊢ \{y \in On \| x \in R_{1} (suc y)\} = \emptyset \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} = V$
27	26	eqeq1d	$⊢ \{y \in On \| x \in R_{1} (suc y)\} = \emptyset \to (⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \leftrightarrow V = 1_{𝑜})$
28	23 27	mtbiri	$⊢ \{y \in On \| x \in R_{1} (suc y)\} = \emptyset \to \neg ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜}$
29	28	necon2ai	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset$
30		onint	$⊢ (\{y \in On \| x \in R_{1} (suc y)\} \subseteq On \land \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset) \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in \{y \in On \| x \in R_{1} (suc y)\}$
31	18 29 30	sylancr	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in \{y \in On \| x \in R_{1} (suc y)\}$
32		eleq1	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to (⋂ \{y \in On \| x \in R_{1} (suc y)\} \in \{y \in On \| x \in R_{1} (suc y)\} \leftrightarrow 1_{𝑜} \in \{y \in On \| x \in R_{1} (suc y)\})$
33	31 32	mpbid	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to 1_{𝑜} \in \{y \in On \| x \in R_{1} (suc y)\}$
34		suceq	$⊢ y = 1_{𝑜} \to suc y = suc 1_{𝑜}$
35	34	fveq2d	$⊢ y = 1_{𝑜} \to R_{1} (suc y) = R_{1} (suc 1_{𝑜})$
36		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
37	36	fveq2i	$⊢ R_{1} (1_{𝑜}) = R_{1} (suc \emptyset)$
38		0elon	$⊢ \emptyset \in On$
39		r1suc	$⊢ \emptyset \in On \to R_{1} (suc \emptyset) = 𝒫 R_{1} (\emptyset)$
40	38 39	ax-mp	$⊢ R_{1} (suc \emptyset) = 𝒫 R_{1} (\emptyset)$
41		r10	$⊢ R_{1} (\emptyset) = \emptyset$
42	41	pweqi	$⊢ 𝒫 R_{1} (\emptyset) = 𝒫 \emptyset$
43	37 40 42	3eqtri	$⊢ R_{1} (1_{𝑜}) = 𝒫 \emptyset$
44	43	pweqi	$⊢ 𝒫 R_{1} (1_{𝑜}) = 𝒫 𝒫 \emptyset$
45		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
46	45	pweqi	$⊢ 𝒫 𝒫 \emptyset = 𝒫 \{\emptyset\}$
47		pwpw0	$⊢ 𝒫 \{\emptyset\} = \{\emptyset, \{\emptyset\}\}$
48	44 46 47	3eqtrri	$⊢ \{\emptyset, \{\emptyset\}\} = 𝒫 R_{1} (1_{𝑜})$
49		1on	$⊢ 1_{𝑜} \in On$
50		r1suc	$⊢ 1_{𝑜} \in On \to R_{1} (suc 1_{𝑜}) = 𝒫 R_{1} (1_{𝑜})$
51	49 50	ax-mp	$⊢ R_{1} (suc 1_{𝑜}) = 𝒫 R_{1} (1_{𝑜})$
52	48 51	eqtr4i	$⊢ \{\emptyset, \{\emptyset\}\} = R_{1} (suc 1_{𝑜})$
53	35 52	eqtr4di	$⊢ y = 1_{𝑜} \to R_{1} (suc y) = \{\emptyset, \{\emptyset\}\}$
54	53	eleq2d	$⊢ y = 1_{𝑜} \to (x \in R_{1} (suc y) \leftrightarrow x \in \{\emptyset, \{\emptyset\}\})$
55	54	elrab	$⊢ 1_{𝑜} \in \{y \in On \| x \in R_{1} (suc y)\} \leftrightarrow (1_{𝑜} \in On \land x \in \{\emptyset, \{\emptyset\}\})$
56	33 55	sylib	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to (1_{𝑜} \in On \land x \in \{\emptyset, \{\emptyset\}\})$
57	12	elpr	$⊢ x \in \{\emptyset, \{\emptyset\}\} \leftrightarrow (x = \emptyset \lor x = \{\emptyset\})$
58		df-ne	$⊢ x \neq \emptyset \leftrightarrow \neg x = \emptyset$
59		orel1	$⊢ \neg x = \emptyset \to ((x = \emptyset \lor x = \{\emptyset\}) \to x = \{\emptyset\})$
60	58 59	sylbi	$⊢ x \neq \emptyset \to ((x = \emptyset \lor x = \{\emptyset\}) \to x = \{\emptyset\})$
61		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
62		eqeq2	$⊢ x = \{\emptyset\} \to (1_{𝑜} = x \leftrightarrow 1_{𝑜} = \{\emptyset\})$
63	61 62	mpbiri	$⊢ x = \{\emptyset\} \to 1_{𝑜} = x$
64	63	eqcomd	$⊢ x = \{\emptyset\} \to x = 1_{𝑜}$
65	60 64	syl6com	$⊢ (x = \emptyset \lor x = \{\emptyset\}) \to (x \neq \emptyset \to x = 1_{𝑜})$
66	57 65	sylbi	$⊢ x \in \{\emptyset, \{\emptyset\}\} \to (x \neq \emptyset \to x = 1_{𝑜})$
67	56 66	simpl2im	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} = 1_{𝑜} \to (x \neq \emptyset \to x = 1_{𝑜})$
68	17 67	sylbi	$⊢ rank (x) = 1_{𝑜} \to (x \neq \emptyset \to x = 1_{𝑜})$
69	15 68	mpd	$⊢ rank (x) = 1_{𝑜} \to x = 1_{𝑜}$
70	9 69	vtoclg	$⊢ A \in V \to (rank (A) = 1_{𝑜} \to A = 1_{𝑜})$
71	6 70	mpcom	$⊢ rank (A) = 1_{𝑜} \to A = 1_{𝑜}$
72		fveq2	$⊢ A = 1_{𝑜} \to rank (A) = rank (1_{𝑜})$
73		r1fnon	$⊢ R_{1} Fn On$
74	73	fndmi	$⊢ dom R_{1} = On$
75	49 74	eleqtrri	$⊢ 1_{𝑜} \in dom R_{1}$
76		rankonid	$⊢ 1_{𝑜} \in dom R_{1} \leftrightarrow rank (1_{𝑜}) = 1_{𝑜}$
77	75 76	mpbi	$⊢ rank (1_{𝑜}) = 1_{𝑜}$
78	72 77	eqtrdi	$⊢ A = 1_{𝑜} \to rank (A) = 1_{𝑜}$
79	71 78	impbii	$⊢ rank (A) = 1_{𝑜} \leftrightarrow A = 1_{𝑜}$
80	61	eqeq2i	$⊢ A = 1_{𝑜} \leftrightarrow A = \{\emptyset\}$
81	79 80	bitri	$⊢ rank (A) = 1_{𝑜} \leftrightarrow A = \{\emptyset\}$

Metamath Proof Explorer

Theorem rankeq1o

Proof