cfeq0

Description: Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

		Ref	Expression
	Assertion	cfeq0	$⊢ A \in On \to (cf (A) = \emptyset \leftrightarrow A = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		cfval	$⊢ A \in On \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
2	1	eqeq1d	$⊢ A \in On \to (cf (A) = \emptyset \leftrightarrow ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} = \emptyset)$
3		vex	$⊢ v \in V$
4		eqeq1	$⊢ x = v \to (x = card (y) \leftrightarrow v = card (y))$
5	4	anbi1d	$⊢ x = v \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow (v = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
6	5	exbidv	$⊢ x = v \to (\exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow \exists y (v = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
7	3 6	elab	$⊢ v \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \leftrightarrow \exists y (v = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
8		fveq2	$⊢ v = card (y) \to card (v) = card (card (y))$
9		cardidm	$⊢ card (card (y)) = card (y)$
10	8 9	syl6eq	$⊢ v = card (y) \to card (v) = card (y)$
11		eqeq2	$⊢ v = card (y) \to (card (v) = v \leftrightarrow card (v) = card (y))$
12	10 11	mpbird	$⊢ v = card (y) \to card (v) = v$
13	12	adantr	$⊢ (v = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to card (v) = v$
14	13	exlimiv	$⊢ \exists y (v = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to card (v) = v$
15	7 14	sylbi	$⊢ v \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \to card (v) = v$
16		cardon	$⊢ card (v) \in On$
17	15 16	eqeltrrdi	$⊢ v \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \to v \in On$
18	17	ssriv	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \subseteq On$
19		onint0	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \subseteq On \to (⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} = \emptyset \leftrightarrow \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\})$
20	18 19	ax-mp	$⊢ ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} = \emptyset \leftrightarrow \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
21		0ex	$⊢ \emptyset \in V$
22		eqeq1	$⊢ x = \emptyset \to (x = card (y) \leftrightarrow \emptyset = card (y))$
23	22	anbi1d	$⊢ x = \emptyset \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow (\emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
24	23	exbidv	$⊢ x = \emptyset \to (\exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow \exists y (\emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
25	21 24	elab	$⊢ \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \leftrightarrow \exists y (\emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
26		onss	$⊢ A \in On \to A \subseteq On$
27		sstr	$⊢ (y \subseteq A \land A \subseteq On) \to y \subseteq On$
28	27	ancoms	$⊢ (A \subseteq On \land y \subseteq A) \to y \subseteq On$
29	26 28	sylan	$⊢ (A \in On \land y \subseteq A) \to y \subseteq On$
30	29	3adant2	$⊢ (A \in On \land \emptyset = card (y) \land y \subseteq A) \to y \subseteq On$
31	30	3adant3r	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to y \subseteq On$
32		simp2	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to \emptyset = card (y)$
33		simp3	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)$
34		eqcom	$⊢ \emptyset = card (y) \leftrightarrow card (y) = \emptyset$
35		vex	$⊢ y \in V$
36		onssnum	$⊢ (y \in V \land y \subseteq On) \to y \in dom card$
37	35 36	mpan	$⊢ y \subseteq On \to y \in dom card$
38		cardnueq0	$⊢ y \in dom card \to (card (y) = \emptyset \leftrightarrow y = \emptyset)$
39	37 38	syl	$⊢ y \subseteq On \to (card (y) = \emptyset \leftrightarrow y = \emptyset)$
40	34 39	syl5bb	$⊢ y \subseteq On \to (\emptyset = card (y) \leftrightarrow y = \emptyset)$
41	40	biimpa	$⊢ (y \subseteq On \land \emptyset = card (y)) \to y = \emptyset$
42		sseq1	$⊢ y = \emptyset \to (y \subseteq A \leftrightarrow \emptyset \subseteq A)$
43		rexeq	$⊢ y = \emptyset \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in \emptyset z \subseteq w)$
44	43	ralbidv	$⊢ y = \emptyset \to (\forall z \in A \exists w \in y z \subseteq w \leftrightarrow \forall z \in A \exists w \in \emptyset z \subseteq w)$
45	42 44	anbi12d	$⊢ y = \emptyset \to ((y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w) \leftrightarrow (\emptyset \subseteq A \land \forall z \in A \exists w \in \emptyset z \subseteq w))$
46	45	biimpa	$⊢ (y = \emptyset \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to (\emptyset \subseteq A \land \forall z \in A \exists w \in \emptyset z \subseteq w)$
47	41 46	sylan	$⊢ ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to (\emptyset \subseteq A \land \forall z \in A \exists w \in \emptyset z \subseteq w)$
48		rex0	$⊢ \neg \exists w \in \emptyset z \subseteq w$
49	48	rgenw	$⊢ \forall z \in A \neg \exists w \in \emptyset z \subseteq w$
50		r19.2z	$⊢ (A \neq \emptyset \land \forall z \in A \neg \exists w \in \emptyset z \subseteq w) \to \exists z \in A \neg \exists w \in \emptyset z \subseteq w$
51	49 50	mpan2	$⊢ A \neq \emptyset \to \exists z \in A \neg \exists w \in \emptyset z \subseteq w$
52		rexnal	$⊢ \exists z \in A \neg \exists w \in \emptyset z \subseteq w \leftrightarrow \neg \forall z \in A \exists w \in \emptyset z \subseteq w$
53	51 52	sylib	$⊢ A \neq \emptyset \to \neg \forall z \in A \exists w \in \emptyset z \subseteq w$
54	53	necon4ai	$⊢ \forall z \in A \exists w \in \emptyset z \subseteq w \to A = \emptyset$
55	47 54	simpl2im	$⊢ ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to A = \emptyset$
56	31 32 33 55	syl21anc	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to A = \emptyset$
57	56	3expib	$⊢ A \in On \to ((\emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to A = \emptyset)$
58	57	exlimdv	$⊢ A \in On \to (\exists y (\emptyset = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to A = \emptyset)$
59	25 58	syl5bi	$⊢ A \in On \to (\emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \to A = \emptyset)$
60	20 59	syl5bi	$⊢ A \in On \to (⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} = \emptyset \to A = \emptyset)$
61	2 60	sylbid	$⊢ A \in On \to (cf (A) = \emptyset \to A = \emptyset)$
62		fveq2	$⊢ A = \emptyset \to cf (A) = cf (\emptyset)$
63		cf0	$⊢ cf (\emptyset) = \emptyset$
64	62 63	syl6eq	$⊢ A = \emptyset \to cf (A) = \emptyset$
65	61 64	impbid1	$⊢ A \in On \to (cf (A) = \emptyset \leftrightarrow A = \emptyset)$

Metamath Proof Explorer

Theorem cfeq0

Proof