Theorem cfsuc 9525

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.)

Assertion

Ref	Expression
cfsuc	⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = 1o)

Proof of Theorem cfsuc

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sucelon 7388	. . 3 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)
2		cfval 9515	. . 3 ⊢ (suc 𝐴 ∈ On → (cf‘suc 𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
3	1, 2	sylbi 218	. 2 ⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
4		cardsn 9244	. . . . . 6 ⊢ (𝐴 ∈ On → (card‘{𝐴}) = 1o)
5	4	eqcomd 2801	. . . . 5 ⊢ (𝐴 ∈ On → 1o = (card‘{𝐴}))
6		snidg 4504	. . . . . . . 8 ⊢ (𝐴 ∈ On → 𝐴 ∈ {𝐴})
7		elsuci 6132	. . . . . . . . 9 ⊢ (𝑧 ∈ suc 𝐴 → (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴))
8		onelss 6108	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → (𝑧 ∈ 𝐴 → 𝑧 ⊆ 𝐴))
9		eqimss 3944	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴)
10	9	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴))
11	8, 10	jaod 854	. . . . . . . . 9 ⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴) → 𝑧 ⊆ 𝐴))
12	7, 11	syl5 34	. . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → 𝑧 ⊆ 𝐴))
13		sseq2 3914	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → (𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝐴))
14	13	rspcev 3559	. . . . . . . 8 ⊢ ((𝐴 ∈ {𝐴} ∧ 𝑧 ⊆ 𝐴) → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)
15	6, 12, 14	syl6an 680	. . . . . . 7 ⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))
16	15	ralrimiv 3148	. . . . . 6 ⊢ (𝐴 ∈ On → ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)
17		ssun2 4070	. . . . . . 7 ⊢ {𝐴} ⊆ (𝐴 ∪ {𝐴})
18		df-suc 6072	. . . . . . 7 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
19	17, 18	sseqtr4i 3925	. . . . . 6 ⊢ {𝐴} ⊆ suc 𝐴
20	16, 19	jctil 520	. . . . 5 ⊢ (𝐴 ∈ On → ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))
21		snex 5223	. . . . . 6 ⊢ {𝐴} ∈ V
22		fveq2 6538	. . . . . . . 8 ⊢ (𝑦 = {𝐴} → (card‘𝑦) = (card‘{𝐴}))
23	22	eqeq2d 2805	. . . . . . 7 ⊢ (𝑦 = {𝐴} → (1o = (card‘𝑦) ↔ 1o = (card‘{𝐴})))
24		sseq1 3913	. . . . . . . 8 ⊢ (𝑦 = {𝐴} → (𝑦 ⊆ suc 𝐴 ↔ {𝐴} ⊆ suc 𝐴))
25		rexeq 3366	. . . . . . . . 9 ⊢ (𝑦 = {𝐴} → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))
26	25	ralbidv 3164	. . . . . . . 8 ⊢ (𝑦 = {𝐴} → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))
27	24, 26	anbi12d 630	. . . . . . 7 ⊢ (𝑦 = {𝐴} → ((𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) ↔ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)))
28	23, 27	anbi12d 630	. . . . . 6 ⊢ (𝑦 = {𝐴} → ((1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1o = (card‘{𝐴}) ∧ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))))
29	21, 28	spcev 3549	. . . . 5 ⊢ ((1o = (card‘{𝐴}) ∧ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) → ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
30	5, 20, 29	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ On → ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
31		1oex 7961	. . . . 5 ⊢ 1o ∈ V
32		eqeq1 2799	. . . . . . 7 ⊢ (𝑥 = 1o → (𝑥 = (card‘𝑦) ↔ 1o = (card‘𝑦)))
33	32	anbi1d 629	. . . . . 6 ⊢ (𝑥 = 1o → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))))
34	33	exbidv 1899	. . . . 5 ⊢ (𝑥 = 1o → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))))
35	31, 34	elab 3605	. . . 4 ⊢ (1o ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
36	30, 35	sylibr 235	. . 3 ⊢ (𝐴 ∈ On → 1o ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
37		el1o 7975	. . . . 5 ⊢ (𝑣 ∈ 1o ↔ 𝑣 = ∅)
38		eqcom 2802	. . . . . . . . . . . . . . 15 ⊢ (∅ = (card‘𝑦) ↔ (card‘𝑦) = ∅)
39		vex 3440	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
40		onssnum 9312	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
41	39, 40	mpan 686	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ On → 𝑦 ∈ dom card)
42		cardnueq0 9239	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ dom card → ((card‘𝑦) = ∅ ↔ 𝑦 = ∅))
43	41, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ On → ((card‘𝑦) = ∅ ↔ 𝑦 = ∅))
44	38, 43	syl5bb 284	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ On → (∅ = (card‘𝑦) ↔ 𝑦 = ∅))
45	44	biimpa 477	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) → 𝑦 = ∅)
46		rex0 4237	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ suc 𝐴 → ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)
48	47	nrex 3232	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
49		nsuceq0 6146	. . . . . . . . . . . . . . . 16 ⊢ suc 𝐴 ≠ ∅
50		r19.2z 4354	. . . . . . . . . . . . . . . 16 ⊢ ((suc 𝐴 ≠ ∅ ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)
51	49, 50	mpan 686	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)
52	48, 51	mto 198	. . . . . . . . . . . . . 14 ⊢ ¬ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
53		rexeq 3366	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ∅ → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤))
54	53	ralbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤))
55	52, 54	mtbiri 328	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → ¬ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)
56	45, 55	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) → ¬ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)
57	56	intnand 489	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) → ¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))
58		imnan 400	. . . . . . . . . . 11 ⊢ (((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) → ¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ¬ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
59	57, 58	mpbi 231	. . . . . . . . . 10 ⊢ ¬ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))
60		suceloni 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)
61		onss 7361	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝐴 ∈ On → suc 𝐴 ⊆ On)
62		sstr 3897	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ⊆ On) → 𝑦 ⊆ On)
63	61, 62	sylan2 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ∈ On) → 𝑦 ⊆ On)
64	60, 63	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ suc 𝐴 ∧ 𝐴 ∈ On) → 𝑦 ⊆ On)
65	64	ancoms 459	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ 𝑦 ⊆ suc 𝐴) → 𝑦 ⊆ On)
66	65	adantrr 713	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ On ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On)
67	66	3adant2 1124	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On)
68		simp2 1130	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∅ = (card‘𝑦))
69		simp3 1131	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))
70	67, 68, 69	jca31 515	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
71	70	3expib 1115	. . . . . . . . . 10 ⊢ (𝐴 ∈ On → ((∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))))
72	59, 71	mtoi 200	. . . . . . . . 9 ⊢ (𝐴 ∈ On → ¬ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
73	72	nexdv 1914	. . . . . . . 8 ⊢ (𝐴 ∈ On → ¬ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
74		0ex 5102	. . . . . . . . 9 ⊢ ∅ ∈ V
75		eqeq1 2799	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ = (card‘𝑦)))
76	75	anbi1d 629	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))))
77	76	exbidv 1899	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))))
78	74, 77	elab 3605	. . . . . . . 8 ⊢ (∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
79	73, 78	sylnibr 330	. . . . . . 7 ⊢ (𝐴 ∈ On → ¬ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
80	79	adantr 481	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
81		eleq1 2870	. . . . . . 7 ⊢ (𝑣 = ∅ → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}))
82	81	adantl 482	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}))
83	80, 82	mtbird 326	. . . . 5 ⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
84	37, 83	sylan2b 593	. . . 4 ⊢ ((𝐴 ∈ On ∧ 𝑣 ∈ 1o) → ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
85	84	ralrimiva 3149	. . 3 ⊢ (𝐴 ∈ On → ∀𝑣 ∈ 1o ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
86		cardon 9219	. . . . . . . 8 ⊢ (card‘𝑦) ∈ On
87		eleq1 2870	. . . . . . . 8 ⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On))
88	86, 87	mpbiri 259	. . . . . . 7 ⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On)
89	88	adantr 481	. . . . . 6 ⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On)
90	89	exlimiv 1908	. . . . 5 ⊢ (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On)
91	90	abssi 3967	. . . 4 ⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On
92		oneqmini 6117	. . . 4 ⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On → ((1o ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∧ ∀𝑣 ∈ 1o ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) → 1o = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}))
93	91, 92	ax-mp 5	. . 3 ⊢ ((1o ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∧ ∀𝑣 ∈ 1o ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) → 1o = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
94	36, 85, 93	syl2anc 584	. 2 ⊢ (𝐴 ∈ On → 1o = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
95	3, 94	eqtr4d 2834	1 ⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = 1o)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1522  ∃wex 1761   ∈ wcel 2081  {cab 2775   ≠ wne 2984  ∀wral 3105  ∃wrex 3106  Vcvv 3437   ∪ cun 3857   ⊆ wss 3859  ∅c0 4211  {csn 4472  ∩ cint 4782  dom cdm 5443  Oncon0 6066  suc csuc 6068  ‘cfv 6225  1_oc1o 7946  cardccrd 9210  cfccf 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-om 7437  df-wrecs 7798  df-recs 7860  df-1o 7953  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-card 9214  df-cf 9216

This theorem is referenced by:  cflim2  9531  cfpwsdom  9852  rankcf  10045