cfsuc

Description: Value of the cofinality function at a successor ordinal. Exercise 3 of TakeutiZaring p. 102. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

		Ref	Expression
	Assertion	cfsuc	$⊢ A \in On \to cf (suc A) = 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		sucelon	$⊢ A \in On \leftrightarrow suc A \in On$
2		cfval	$⊢ suc A \in On \to cf (suc A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
3	1 2	sylbi	$⊢ A \in On \to cf (suc A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
4		cardsn	$⊢ A \in On \to card (\{A\}) = 1_{𝑜}$
5	4	eqcomd	$⊢ A \in On \to 1_{𝑜} = card (\{A\})$
6		snidg	$⊢ A \in On \to A \in \{A\}$
7		elsuci	$⊢ z \in suc A \to (z \in A \lor z = A)$
8		onelss	$⊢ A \in On \to (z \in A \to z \subseteq A)$
9		eqimss	$⊢ z = A \to z \subseteq A$
10	9	a1i	$⊢ A \in On \to (z = A \to z \subseteq A)$
11	8 10	jaod	$⊢ A \in On \to ((z \in A \lor z = A) \to z \subseteq A)$
12	7 11	syl5	$⊢ A \in On \to (z \in suc A \to z \subseteq A)$
13		sseq2	$⊢ w = A \to (z \subseteq w \leftrightarrow z \subseteq A)$
14	13	rspcev	$⊢ (A \in \{A\} \land z \subseteq A) \to \exists w \in \{A\} z \subseteq w$
15	6 12 14	syl6an	$⊢ A \in On \to (z \in suc A \to \exists w \in \{A\} z \subseteq w)$
16	15	ralrimiv	$⊢ A \in On \to \forall z \in suc A \exists w \in \{A\} z \subseteq w$
17		ssun2	$⊢ \{A\} \subseteq A \cup \{A\}$
18		df-suc	$⊢ suc A = A \cup \{A\}$
19	17 18	sseqtrri	$⊢ \{A\} \subseteq suc A$
20	16 19	jctil	$⊢ A \in On \to (\{A\} \subseteq suc A \land \forall z \in suc A \exists w \in \{A\} z \subseteq w)$
21		snex	$⊢ \{A\} \in V$
22		fveq2	$⊢ y = \{A\} \to card (y) = card (\{A\})$
23	22	eqeq2d	$⊢ y = \{A\} \to (1_{𝑜} = card (y) \leftrightarrow 1_{𝑜} = card (\{A\}))$
24		sseq1	$⊢ y = \{A\} \to (y \subseteq suc A \leftrightarrow \{A\} \subseteq suc A)$
25		rexeq	$⊢ y = \{A\} \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in \{A\} z \subseteq w)$
26	25	ralbidv	$⊢ y = \{A\} \to (\forall z \in suc A \exists w \in y z \subseteq w \leftrightarrow \forall z \in suc A \exists w \in \{A\} z \subseteq w)$
27	24 26	anbi12d	$⊢ y = \{A\} \to ((y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w) \leftrightarrow (\{A\} \subseteq suc A \land \forall z \in suc A \exists w \in \{A\} z \subseteq w))$
28	23 27	anbi12d	$⊢ y = \{A\} \to ((1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow (1_{𝑜} = card (\{A\}) \land (\{A\} \subseteq suc A \land \forall z \in suc A \exists w \in \{A\} z \subseteq w)))$
29	21 28	spcev	$⊢ (1_{𝑜} = card (\{A\}) \land (\{A\} \subseteq suc A \land \forall z \in suc A \exists w \in \{A\} z \subseteq w)) \to \exists y (1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
30	5 20 29	syl2anc	$⊢ A \in On \to \exists y (1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
31		1oex	$⊢ 1_{𝑜} \in V$
32		eqeq1	$⊢ x = 1_{𝑜} \to (x = card (y) \leftrightarrow 1_{𝑜} = card (y))$
33	32	anbi1d	$⊢ x = 1_{𝑜} \to ((x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow (1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)))$
34	33	exbidv	$⊢ x = 1_{𝑜} \to (\exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow \exists y (1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)))$
35	31 34	elab	$⊢ 1_{𝑜} \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \leftrightarrow \exists y (1_{𝑜} = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
36	30 35	sylibr	$⊢ A \in On \to 1_{𝑜} \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
37		el1o	$⊢ v \in 1_{𝑜} \leftrightarrow v = \emptyset$
38		eqcom	$⊢ \emptyset = card (y) \leftrightarrow card (y) = \emptyset$
39		vex	$⊢ y \in V$
40		onssnum	$⊢ (y \in V \land y \subseteq On) \to y \in dom card$
41	39 40	mpan	$⊢ y \subseteq On \to y \in dom card$
42		cardnueq0	$⊢ y \in dom card \to (card (y) = \emptyset \leftrightarrow y = \emptyset)$
43	41 42	syl	$⊢ y \subseteq On \to (card (y) = \emptyset \leftrightarrow y = \emptyset)$
44	38 43	bitrid	$⊢ y \subseteq On \to (\emptyset = card (y) \leftrightarrow y = \emptyset)$
45	44	biimpa	$⊢ (y \subseteq On \land \emptyset = card (y)) \to y = \emptyset$
46		rex0	$⊢ \neg \exists w \in \emptyset z \subseteq w$
47	46	a1i	$⊢ z \in suc A \to \neg \exists w \in \emptyset z \subseteq w$
48	47	nrex	$⊢ \neg \exists z \in suc A \exists w \in \emptyset z \subseteq w$
49		nsuceq0	$⊢ suc A \neq \emptyset$
50		r19.2z	$⊢ (suc A \neq \emptyset \land \forall z \in suc A \exists w \in \emptyset z \subseteq w) \to \exists z \in suc A \exists w \in \emptyset z \subseteq w$
51	49 50	mpan	$⊢ \forall z \in suc A \exists w \in \emptyset z \subseteq w \to \exists z \in suc A \exists w \in \emptyset z \subseteq w$
52	48 51	mto	$⊢ \neg \forall z \in suc A \exists w \in \emptyset z \subseteq w$
53		rexeq	$⊢ y = \emptyset \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in \emptyset z \subseteq w)$
54	53	ralbidv	$⊢ y = \emptyset \to (\forall z \in suc A \exists w \in y z \subseteq w \leftrightarrow \forall z \in suc A \exists w \in \emptyset z \subseteq w)$
55	52 54	mtbiri	$⊢ y = \emptyset \to \neg \forall z \in suc A \exists w \in y z \subseteq w$
56	45 55	syl	$⊢ (y \subseteq On \land \emptyset = card (y)) \to \neg \forall z \in suc A \exists w \in y z \subseteq w$
57	56	intnand	$⊢ (y \subseteq On \land \emptyset = card (y)) \to \neg (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)$
58		imnan	$⊢ ((y \subseteq On \land \emptyset = card (y)) \to \neg (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow \neg ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
59	57 58	mpbi	$⊢ \neg ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
60		suceloni	$⊢ A \in On \to suc A \in On$
61		onss	$⊢ suc A \in On \to suc A \subseteq On$
62		sstr	$⊢ (y \subseteq suc A \land suc A \subseteq On) \to y \subseteq On$
63	61 62	sylan2	$⊢ (y \subseteq suc A \land suc A \in On) \to y \subseteq On$
64	60 63	sylan2	$⊢ (y \subseteq suc A \land A \in On) \to y \subseteq On$
65	64	ancoms	$⊢ (A \in On \land y \subseteq suc A) \to y \subseteq On$
66	65	adantrr	$⊢ (A \in On \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to y \subseteq On$
67	66	3adant2	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to y \subseteq On$
68		simp2	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to \emptyset = card (y)$
69		simp3	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)$
70	67 68 69	jca31	$⊢ (A \in On \land \emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
71	70	3expib	$⊢ A \in On \to ((\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to ((y \subseteq On \land \emptyset = card (y)) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)))$
72	59 71	mtoi	$⊢ A \in On \to \neg (\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
73	72	nexdv	$⊢ A \in On \to \neg \exists y (\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
74		0ex	$⊢ \emptyset \in V$
75		eqeq1	$⊢ x = \emptyset \to (x = card (y) \leftrightarrow \emptyset = card (y))$
76	75	anbi1d	$⊢ x = \emptyset \to ((x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow (\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)))$
77	76	exbidv	$⊢ x = \emptyset \to (\exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \leftrightarrow \exists y (\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)))$
78	74 77	elab	$⊢ \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \leftrightarrow \exists y (\emptyset = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))$
79	73 78	sylnibr	$⊢ A \in On \to \neg \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
80	79	adantr	$⊢ (A \in On \land v = \emptyset) \to \neg \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
81		eleq1	$⊢ v = \emptyset \to (v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \leftrightarrow \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\})$
82	81	adantl	$⊢ (A \in On \land v = \emptyset) \to (v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \leftrightarrow \emptyset \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\})$
83	80 82	mtbird	$⊢ (A \in On \land v = \emptyset) \to \neg v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
84	37 83	sylan2b	$⊢ (A \in On \land v \in 1_{𝑜}) \to \neg v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
85	84	ralrimiva	$⊢ A \in On \to \forall v \in 1_{𝑜} \neg v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
86		cardon	$⊢ card (y) \in On$
87		eleq1	$⊢ x = card (y) \to (x \in On \leftrightarrow card (y) \in On)$
88	86 87	mpbiri	$⊢ x = card (y) \to x \in On$
89	88	adantr	$⊢ (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to x \in On$
90	89	exlimiv	$⊢ \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w)) \to x \in On$
91	90	abssi	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \subseteq On$
92		oneqmini	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \subseteq On \to ((1_{𝑜} \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \land \forall v \in 1_{𝑜} \neg v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}) \to 1_{𝑜} = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\})$
93	91 92	ax-mp	$⊢ (1_{𝑜} \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\} \land \forall v \in 1_{𝑜} \neg v \in \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}) \to 1_{𝑜} = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
94	36 85 93	syl2anc	$⊢ A \in On \to 1_{𝑜} = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq suc A \land \forall z \in suc A \exists w \in y z \subseteq w))\}$
95	3 94	eqtr4d	$⊢ A \in On \to cf (suc A) = 1_{𝑜}$

Metamath Proof Explorer

Theorem cfsuc

Proof