Step | Hyp | Ref
| Expression |
1 | | sucelon 7017 |
. . 3
⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On) |
2 | | cfval 9069 |
. . 3
⊢ (suc
𝐴 ∈ On →
(cf‘suc 𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
3 | 1, 2 | sylbi 207 |
. 2
⊢ (𝐴 ∈ On → (cf‘suc
𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
4 | | cardsn 8795 |
. . . . . 6
⊢ (𝐴 ∈ On →
(card‘{𝐴}) =
1𝑜) |
5 | 4 | eqcomd 2628 |
. . . . 5
⊢ (𝐴 ∈ On →
1𝑜 = (card‘{𝐴})) |
6 | | snidg 4206 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ∈ {𝐴}) |
7 | | elsuci 5791 |
. . . . . . . . 9
⊢ (𝑧 ∈ suc 𝐴 → (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴)) |
8 | | onelss 5766 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑧 ∈ 𝐴 → 𝑧 ⊆ 𝐴)) |
9 | | eqimss 3657 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴) |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝑧 = 𝐴 → 𝑧 ⊆ 𝐴)) |
11 | 8, 10 | jaod 395 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ((𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐴) → 𝑧 ⊆ 𝐴)) |
12 | 7, 11 | syl5 34 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → 𝑧 ⊆ 𝐴)) |
13 | | sseq2 3627 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝐴)) |
14 | 13 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝐴 ∈ {𝐴} ∧ 𝑧 ⊆ 𝐴) → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤) |
15 | 6, 12, 14 | syl6an 568 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝑧 ∈ suc 𝐴 → ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
16 | 15 | ralrimiv 2965 |
. . . . . 6
⊢ (𝐴 ∈ On → ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤) |
17 | | ssun2 3777 |
. . . . . . 7
⊢ {𝐴} ⊆ (𝐴 ∪ {𝐴}) |
18 | | df-suc 5729 |
. . . . . . 7
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
19 | 17, 18 | sseqtr4i 3638 |
. . . . . 6
⊢ {𝐴} ⊆ suc 𝐴 |
20 | 16, 19 | jctil 560 |
. . . . 5
⊢ (𝐴 ∈ On → ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
21 | | snex 4908 |
. . . . . 6
⊢ {𝐴} ∈ V |
22 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (card‘𝑦) = (card‘{𝐴})) |
23 | 22 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑦 = {𝐴} → (1𝑜 =
(card‘𝑦) ↔
1𝑜 = (card‘{𝐴}))) |
24 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (𝑦 ⊆ suc 𝐴 ↔ {𝐴} ⊆ suc 𝐴)) |
25 | | rexeq 3139 |
. . . . . . . . 9
⊢ (𝑦 = {𝐴} → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
26 | 25 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑦 = {𝐴} → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) |
27 | 24, 26 | anbi12d 747 |
. . . . . . 7
⊢ (𝑦 = {𝐴} → ((𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) ↔ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤))) |
28 | 23, 27 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = {𝐴} → ((1𝑜 =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1𝑜 =
(card‘{𝐴}) ∧
({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)))) |
29 | 21, 28 | spcev 3300 |
. . . . 5
⊢
((1𝑜 = (card‘{𝐴}) ∧ ({𝐴} ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ {𝐴}𝑧 ⊆ 𝑤)) → ∃𝑦(1𝑜 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
30 | 5, 20, 29 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ On → ∃𝑦(1𝑜 =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
31 | | 1on 7567 |
. . . . . 6
⊢
1𝑜 ∈ On |
32 | 31 | elexi 3213 |
. . . . 5
⊢
1𝑜 ∈ V |
33 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑥 = 1𝑜 →
(𝑥 = (card‘𝑦) ↔ 1𝑜 =
(card‘𝑦))) |
34 | 33 | anbi1d 741 |
. . . . . 6
⊢ (𝑥 = 1𝑜 →
((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (1𝑜 =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
35 | 34 | exbidv 1850 |
. . . . 5
⊢ (𝑥 = 1𝑜 →
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(1𝑜 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
36 | 32, 35 | elab 3350 |
. . . 4
⊢
(1𝑜 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(1𝑜 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
37 | 30, 36 | sylibr 224 |
. . 3
⊢ (𝐴 ∈ On →
1𝑜 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
38 | | el1o 7579 |
. . . . 5
⊢ (𝑣 ∈ 1𝑜
↔ 𝑣 =
∅) |
39 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
⊢ (∅
= (card‘𝑦) ↔
(card‘𝑦) =
∅) |
40 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
41 | | onssnum 8863 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
42 | 40, 41 | mpan 706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
43 | | cardnueq0 8790 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ dom card →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ On →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
45 | 39, 44 | syl5bb 272 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ On → (∅ =
(card‘𝑦) ↔ 𝑦 = ∅)) |
46 | 45 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
𝑦 =
∅) |
47 | | rex0 3938 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
∃𝑤 ∈ ∅
𝑧 ⊆ 𝑤 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ suc 𝐴 → ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
49 | 48 | nrex 3000 |
. . . . . . . . . . . . . . 15
⊢ ¬
∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
50 | | nsuceq0 5805 |
. . . . . . . . . . . . . . . 16
⊢ suc 𝐴 ≠ ∅ |
51 | | r19.2z 4060 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝐴 ≠ ∅ ∧
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
52 | 50, 51 | mpan 706 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → ∃𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
53 | 49, 52 | mto 188 |
. . . . . . . . . . . . . 14
⊢ ¬
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
54 | | rexeq 3139 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ∅ → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
55 | 54 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∅ → (∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
56 | 53, 55 | mtbiri 317 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → ¬
∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) |
57 | 46, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ ∀𝑧 ∈ suc
𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) |
58 | 57 | intnand 962 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
59 | | imnan 438 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
¬ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ¬ ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
60 | 58, 59 | mpbi 220 |
. . . . . . . . . 10
⊢ ¬
((𝑦 ⊆ On ∧
∅ = (card‘𝑦))
∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
61 | | suceloni 7013 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
62 | | onss 6990 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝐴 ∈ On → suc
𝐴 ⊆
On) |
63 | | sstr 3611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ⊆ On) → 𝑦 ⊆ On) |
64 | 62, 63 | sylan2 491 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ suc 𝐴 ∧ suc 𝐴 ∈ On) → 𝑦 ⊆ On) |
65 | 61, 64 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ suc 𝐴 ∧ 𝐴 ∈ On) → 𝑦 ⊆ On) |
66 | 65 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑦 ⊆ suc 𝐴) → 𝑦 ⊆ On) |
67 | 66 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
68 | 67 | 3adant2 1080 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
69 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∅ = (card‘𝑦)) |
70 | | simp3 1063 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
71 | 68, 69, 70 | jca31 557 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
72 | 71 | 3expib 1268 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → ((∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
73 | 60, 72 | mtoi 190 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ¬ (∅
= (card‘𝑦) ∧
(𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
74 | 73 | nexdv 1864 |
. . . . . . . 8
⊢ (𝐴 ∈ On → ¬
∃𝑦(∅ =
(card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
75 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
76 | | eqeq1 2626 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ =
(card‘𝑦))) |
77 | 76 | anbi1d 741 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
78 | 77 | exbidv 1850 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
79 | 75, 78 | elab 3350 |
. . . . . . . 8
⊢ (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
80 | 74, 79 | sylnibr 319 |
. . . . . . 7
⊢ (𝐴 ∈ On → ¬ ∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
81 | 80 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ ∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
82 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑣 = ∅ → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
83 | 82 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
84 | 81, 83 | mtbird 315 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑣 = ∅) → ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
85 | 38, 84 | sylan2b 492 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑣 ∈ 1𝑜)
→ ¬ 𝑣 ∈
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
86 | 85 | ralrimiva 2966 |
. . 3
⊢ (𝐴 ∈ On → ∀𝑣 ∈ 1𝑜
¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
87 | | cardon 8770 |
. . . . . . . 8
⊢
(card‘𝑦)
∈ On |
88 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
89 | 87, 88 | mpbiri 248 |
. . . . . . 7
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
90 | 89 | adantr 481 |
. . . . . 6
⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On) |
91 | 90 | exlimiv 1858 |
. . . . 5
⊢
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑥 ∈ On) |
92 | 91 | abssi 3677 |
. . . 4
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
93 | | oneqmini 5776 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On → ((1𝑜
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∧ ∀𝑣 ∈ 1𝑜 ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) → 1𝑜 = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
94 | 92, 93 | ax-mp 5 |
. . 3
⊢
((1𝑜 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∧ ∀𝑣 ∈ 1𝑜 ¬ 𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) → 1𝑜 = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
95 | 37, 86, 94 | syl2anc 693 |
. 2
⊢ (𝐴 ∈ On →
1𝑜 = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ suc 𝐴 ∧ ∀𝑧 ∈ suc 𝐴∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
96 | 3, 95 | eqtr4d 2659 |
1
⊢ (𝐴 ∈ On → (cf‘suc
𝐴) =
1𝑜) |