Step | Hyp | Ref
| Expression |
1 | | sucelon 7526 |
. . 3
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
2 | | cfval 9663 |
. . 3
⊢ (suc
𝐴 ∈ On →
(cf‘suc 𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
3 | 1, 2 | sylbi 219 |
. 2
⊢ (𝐴 ∈ On → (cf‘suc
𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
4 | | cardsn 9392 |
. . . . . 6
⊢ (𝐴 ∈ On →
(card‘{𝐴}) =
1o) |
5 | 4 | eqcomd 2827 |
. . . . 5
⊢ (𝐴 ∈ On → 1o
= (card‘{𝐴})) |
6 | | snidg 4592 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ∈ {𝐴}) |
7 | | elsuci 6251 |
. . . . . . . . 9
⊢ (𝑧 ∈ suc 𝐴 → (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴)) |
8 | | onelss 6227 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑧 ∈ 𝐴 → 𝑧 ⊆ 𝐴)) |
9 | | eqimss 4022 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴) |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴)) |
11 | 8, 10 | jaod 855 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴) → 𝑧 ⊆ 𝐴)) |
12 | 7, 11 | syl5 34 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → 𝑧 ⊆ 𝐴)) |
13 | | sseq2 3992 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝐴)) |
14 | 13 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝐴 ∈ {𝐴} ∧ 𝑧 ⊆ 𝐴) → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤) |
15 | 6, 12, 14 | syl6an 682 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
16 | 15 | ralrimiv 3181 |
. . . . . 6
⊢ (𝐴 ∈ On → ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤) |
17 | | ssun2 4148 |
. . . . . . 7
⊢ {𝐴} ⊆ (𝐴 ∪ {𝐴}) |
18 | | df-suc 6191 |
. . . . . . 7
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
19 | 17, 18 | sseqtrri 4003 |
. . . . . 6
⊢ {𝐴} ⊆ suc 𝐴 |
20 | 16, 19 | jctil 522 |
. . . . 5
⊢ (𝐴 ∈ On → ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
21 | | snex 5323 |
. . . . . 6
⊢ {𝐴} ∈ V |
22 | | fveq2 6664 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (card‘𝑦) = (card‘{𝐴})) |
23 | 22 | eqeq2d 2832 |
. . . . . . 7
⊢ (𝑦 = {𝐴} → (1o = (card‘𝑦) ↔ 1o =
(card‘{𝐴}))) |
24 | | sseq1 3991 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (𝑦 ⊆ suc 𝐴 ↔ {𝐴} ⊆ suc 𝐴)) |
25 | | rexeq 3406 |
. . . . . . . . 9
⊢ (𝑦 = {𝐴} → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
26 | 25 | ralbidv 3197 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
27 | 24, 26 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = {𝐴} → ((𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) ↔ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))) |
28 | 23, 27 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = {𝐴} → ((1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1o = (card‘{𝐴}) ∧ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)))) |
29 | 21, 28 | spcev 3606 |
. . . . 5
⊢
((1o = (card‘{𝐴}) ∧ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) → ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
30 | 5, 20, 29 | syl2anc 586 |
. . . 4
⊢ (𝐴 ∈ On → ∃𝑦(1o =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
31 | | 1oex 8104 |
. . . . 5
⊢
1o ∈ V |
32 | | eqeq1 2825 |
. . . . . . 7
⊢ (𝑥 = 1o → (𝑥 = (card‘𝑦) ↔ 1o =
(card‘𝑦))) |
33 | 32 | anbi1d 631 |
. . . . . 6
⊢ (𝑥 = 1o → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
34 | 33 | exbidv 1918 |
. . . . 5
⊢ (𝑥 = 1o →
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
35 | 31, 34 | elab 3666 |
. . . 4
⊢
(1o ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(1o = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
36 | 30, 35 | sylibr 236 |
. . 3
⊢ (𝐴 ∈ On → 1o
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
37 | | el1o 8118 |
. . . . 5
⊢ (𝑣 ∈ 1o ↔
𝑣 =
∅) |
38 | | eqcom 2828 |
. . . . . . . . . . . . . . 15
⊢ (∅
= (card‘𝑦) ↔
(card‘𝑦) =
∅) |
39 | | vex 3497 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
40 | | onssnum 9460 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
41 | 39, 40 | mpan 688 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
42 | | cardnueq0 9387 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ dom card →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ On →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
44 | 38, 43 | syl5bb 285 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ On → (∅ =
(card‘𝑦) ↔ 𝑦 = ∅)) |
45 | 44 | biimpa 479 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
𝑦 =
∅) |
46 | | rex0 4316 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
∃𝑤 ∈ ∅
𝑧 ⊆ 𝑤 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ suc 𝐴 → ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
48 | 47 | nrex 3269 |
. . . . . . . . . . . . . . 15
⊢ ¬
∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
49 | | nsuceq0 6265 |
. . . . . . . . . . . . . . . 16
⊢ suc 𝐴 ≠ ∅ |
50 | | r19.2z 4439 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝐴 ≠ ∅ ∧
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
51 | 49, 50 | mpan 688 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
52 | 48, 51 | mto 199 |
. . . . . . . . . . . . . 14
⊢ ¬
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
53 | | rexeq 3406 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
54 | 53 | ralbidv 3197 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
55 | 52, 54 | mtbiri 329 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ¬
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) |
56 | 45, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ ∀𝑧 ∈ suc
𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) |
57 | 56 | intnand 491 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
58 | | imnan 402 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ¬ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
59 | 57, 58 | mpbi 232 |
. . . . . . . . . 10
⊢ ¬
((𝑦 ⊆ On ∧
∅ = (card‘𝑦))
∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
60 | | suceloni 7522 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
61 | | onss 7499 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝐴 ∈ On → suc
𝐴 ⊆
On) |
62 | | sstr 3974 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ⊆ On) → 𝑦 ⊆ On) |
63 | 61, 62 | sylan2 594 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ∈ On) → 𝑦 ⊆ On) |
64 | 60, 63 | sylan2 594 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ suc 𝐴 ∧ 𝐴 ∈ On) → 𝑦 ⊆ On) |
65 | 64 | ancoms 461 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑦 ⊆ suc 𝐴) → 𝑦 ⊆ On) |
66 | 65 | adantrr 715 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
67 | 66 | 3adant2 1127 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
68 | | simp2 1133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∅ = (card‘𝑦)) |
69 | | simp3 1134 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
70 | 67, 68, 69 | jca31 517 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
71 | 70 | 3expib 1118 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → ((∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
72 | 59, 71 | mtoi 201 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ¬ (∅
= (card‘𝑦) ∧
(𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
73 | 72 | nexdv 1933 |
. . . . . . . 8
⊢ (𝐴 ∈ On → ¬
∃𝑦(∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
74 | | 0ex 5203 |
. . . . . . . . 9
⊢ ∅
∈ V |
75 | | eqeq1 2825 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ =
(card‘𝑦))) |
76 | 75 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
77 | 76 | exbidv 1918 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
78 | 74, 77 | elab 3666 |
. . . . . . . 8
⊢ (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
79 | 73, 78 | sylnibr 331 |
. . . . . . 7
⊢ (𝐴 ∈ On → ¬ ∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
80 | 79 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ ∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
81 | | eleq1 2900 |
. . . . . . 7
⊢ (𝑣 = ∅ → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
82 | 81 | adantl 484 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
83 | 80, 82 | mtbird 327 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
84 | 37, 83 | sylan2b 595 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑣 ∈ 1o) →
¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
85 | 84 | ralrimiva 3182 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑣 ∈ 1o ¬
𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
86 | | cardon 9367 |
. . . . . . . 8
⊢
(card‘𝑦)
∈ On |
87 | | eleq1 2900 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
88 | 86, 87 | mpbiri 260 |
. . . . . . 7
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
89 | 88 | adantr 483 |
. . . . . 6
⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On) |
90 | 89 | exlimiv 1927 |
. . . . 5
⊢
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On) |
91 | 90 | abssi 4045 |
. . . 4
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
92 | | oneqmini 6236 |
. . . 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 586 |
. 2
⊢ (𝐴 ∈ On → 1o
= ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
95 | 3, 94 | eqtr4d 2859 |
1
⊢ (𝐴 ∈ On → (cf‘suc
𝐴) =
1o) |