Step | Hyp | Ref
| Expression |
1 | | cfval 9861 |
. . . 4
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
2 | 1 | eqeq1d 2739 |
. . 3
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
↔ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅)) |
3 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
4 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝑥 = (card‘𝑦) ↔ 𝑣 = (card‘𝑦))) |
5 | 4 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
6 | 5 | exbidv 1929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
7 | 3, 6 | elab 3587 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
8 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) =
(card‘(card‘𝑦))) |
9 | | cardidm 9575 |
. . . . . . . . . . . 12
⊢
(card‘(card‘𝑦)) = (card‘𝑦) |
10 | 8, 9 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘𝑦)) |
11 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → ((card‘𝑣) = 𝑣 ↔ (card‘𝑣) = (card‘𝑦))) |
12 | 10, 11 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = 𝑣) |
13 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
14 | 13 | exlimiv 1938 |
. . . . . . . 8
⊢
(∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
15 | 7, 14 | sylbi 220 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘𝑣) = 𝑣) |
16 | | cardon 9560 |
. . . . . . 7
⊢
(card‘𝑣)
∈ On |
17 | 15, 16 | eqeltrrdi 2847 |
. . . . . 6
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝑣 ∈ On) |
18 | 17 | ssriv 3905 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
19 | | onint0 7575 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On → (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
20 | 18, 19 | ax-mp 5 |
. . . 4
⊢ (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
21 | | 0ex 5200 |
. . . . . 6
⊢ ∅
∈ V |
22 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ =
(card‘𝑦))) |
23 | 22 | anbi1d 633 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
24 | 23 | exbidv 1929 |
. . . . . 6
⊢ (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
25 | 21, 24 | elab 3587 |
. . . . 5
⊢ (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
26 | | onss 7568 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
27 | | sstr 3909 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On) |
28 | 27 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
29 | 26, 28 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
30 | 29 | 3adant2 1133 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
31 | 30 | 3adant3r 1183 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
32 | | simp2 1139 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∅ = (card‘𝑦)) |
33 | | simp3 1140 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
34 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (∅
= (card‘𝑦) ↔
(card‘𝑦) =
∅) |
35 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
36 | | onssnum 9654 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
37 | 35, 36 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
38 | | cardnueq0 9580 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ dom card →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ On →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
40 | 34, 39 | syl5bb 286 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ On → (∅ =
(card‘𝑦) ↔ 𝑦 = ∅)) |
41 | 40 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
𝑦 =
∅) |
42 | | sseq1 3926 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (𝑦 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
43 | | rexeq 3320 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
44 | 43 | ralbidv 3118 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
45 | 42, 44 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) ↔ (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤))) |
46 | 45 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
47 | 41, 46 | sylan 583 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) ∧
(𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
48 | | rex0 4272 |
. . . . . . . . . . . . 13
⊢ ¬
∃𝑤 ∈ ∅
𝑧 ⊆ 𝑤 |
49 | 48 | rgenw 3073 |
. . . . . . . . . . . 12
⊢
∀𝑧 ∈
𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
50 | | r19.2z 4406 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) → ∃𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
51 | 49, 50 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ →
∃𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
52 | | rexnal 3160 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ↔ ¬ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
53 | 51, 52 | sylib 221 |
. . . . . . . . . 10
⊢ (𝐴 ≠ ∅ → ¬
∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
54 | 53 | necon4ai 2972 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → 𝐴 = ∅) |
55 | 47, 54 | simpl2im 507 |
. . . . . . . 8
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) ∧
(𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅) |
56 | 31, 32, 33, 55 | syl21anc 838 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅) |
57 | 56 | 3expib 1124 |
. . . . . 6
⊢ (𝐴 ∈ On → ((∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅)) |
58 | 57 | exlimdv 1941 |
. . . . 5
⊢ (𝐴 ∈ On → (∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅)) |
59 | 25, 58 | syl5bi 245 |
. . . 4
⊢ (𝐴 ∈ On → (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝐴 = ∅)) |
60 | 20, 59 | syl5bi 245 |
. . 3
⊢ (𝐴 ∈ On → (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ → 𝐴 = ∅)) |
61 | 2, 60 | sylbid 243 |
. 2
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
→ 𝐴 =
∅)) |
62 | | fveq2 6717 |
. . 3
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
(cf‘∅)) |
63 | | cf0 9865 |
. . 3
⊢
(cf‘∅) = ∅ |
64 | 62, 63 | eqtrdi 2794 |
. 2
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
∅) |
65 | 61, 64 | impbid1 228 |
1
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
↔ 𝐴 =
∅)) |