| Step | Hyp | Ref
| Expression |
| 1 | | cfval 10287 |
. . . 4
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 2 | 1 | eqeq1d 2739 |
. . 3
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
↔ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅)) |
| 3 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
| 4 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝑥 = (card‘𝑦) ↔ 𝑣 = (card‘𝑦))) |
| 5 | 4 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 6 | 5 | exbidv 1921 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 7 | 3, 6 | elab 3679 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
| 8 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) =
(card‘(card‘𝑦))) |
| 9 | | cardidm 9999 |
. . . . . . . . . . . 12
⊢
(card‘(card‘𝑦)) = (card‘𝑦) |
| 10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘𝑦)) |
| 11 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → ((card‘𝑣) = 𝑣 ↔ (card‘𝑣) = (card‘𝑦))) |
| 12 | 10, 11 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = 𝑣) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
| 14 | 13 | exlimiv 1930 |
. . . . . . . 8
⊢
(∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
| 15 | 7, 14 | sylbi 217 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘𝑣) = 𝑣) |
| 16 | | cardon 9984 |
. . . . . . 7
⊢
(card‘𝑣)
∈ On |
| 17 | 15, 16 | eqeltrrdi 2850 |
. . . . . 6
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝑣 ∈ On) |
| 18 | 17 | ssriv 3987 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
| 19 | | onint0 7811 |
. . . . 5
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On → (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})) |
| 20 | 18, 19 | ax-mp 5 |
. . . 4
⊢ (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 21 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 22 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ =
(card‘𝑦))) |
| 23 | 22 | anbi1d 631 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 24 | 23 | exbidv 1921 |
. . . . . 6
⊢ (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 25 | 21, 24 | elab 3679 |
. . . . 5
⊢ (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
| 26 | | onss 7805 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
| 27 | | sstr 3992 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On) |
| 28 | 27 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
| 29 | 26, 28 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
| 30 | 29 | 3adant2 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
| 31 | 30 | 3adant3r 1182 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝑦 ⊆ On) |
| 32 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∅ = (card‘𝑦)) |
| 33 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) |
| 34 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (∅
= (card‘𝑦) ↔
(card‘𝑦) =
∅) |
| 35 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
| 36 | | onssnum 10080 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
| 37 | 35, 36 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
| 38 | | cardnueq0 10004 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ dom card →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ On →
((card‘𝑦) = ∅
↔ 𝑦 =
∅)) |
| 40 | 34, 39 | bitrid 283 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ On → (∅ =
(card‘𝑦) ↔ 𝑦 = ∅)) |
| 41 | 40 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) →
𝑦 =
∅) |
| 42 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (𝑦 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 43 | | rexeq 3322 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
| 44 | 43 | ralbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
| 45 | 42, 44 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) ↔ (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤))) |
| 46 | 45 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
| 47 | 41, 46 | sylan 580 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) ∧
(𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤)) |
| 48 | | rex0 4360 |
. . . . . . . . . . . . 13
⊢ ¬
∃𝑤 ∈ ∅
𝑧 ⊆ 𝑤 |
| 49 | 48 | rgenw 3065 |
. . . . . . . . . . . 12
⊢
∀𝑧 ∈
𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 |
| 50 | | r19.2z 4495 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) → ∃𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
| 51 | 49, 50 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ →
∃𝑧 ∈ 𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
| 52 | | rexnal 3100 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ↔ ¬ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
| 53 | 51, 52 | sylib 218 |
. . . . . . . . . 10
⊢ (𝐴 ≠ ∅ → ¬
∀𝑧 ∈ 𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤) |
| 54 | 53 | necon4ai 2972 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → 𝐴 = ∅) |
| 55 | 47, 54 | simpl2im 503 |
. . . . . . . 8
⊢ (((𝑦 ⊆ On ∧ ∅ =
(card‘𝑦)) ∧
(𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅) |
| 56 | 31, 32, 33, 55 | syl21anc 838 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ ∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅) |
| 57 | 56 | 3expib 1123 |
. . . . . 6
⊢ (𝐴 ∈ On → ((∅ =
(card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅)) |
| 58 | 57 | exlimdv 1933 |
. . . . 5
⊢ (𝐴 ∈ On → (∃𝑦(∅ = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → 𝐴 = ∅)) |
| 59 | 25, 58 | biimtrid 242 |
. . . 4
⊢ (𝐴 ∈ On → (∅
∈ {𝑥 ∣
∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝐴 = ∅)) |
| 60 | 20, 59 | biimtrid 242 |
. . 3
⊢ (𝐴 ∈ On → (∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} = ∅ → 𝐴 = ∅)) |
| 61 | 2, 60 | sylbid 240 |
. 2
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
→ 𝐴 =
∅)) |
| 62 | | fveq2 6906 |
. . 3
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
(cf‘∅)) |
| 63 | | cf0 10291 |
. . 3
⊢
(cf‘∅) = ∅ |
| 64 | 62, 63 | eqtrdi 2793 |
. 2
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
∅) |
| 65 | 61, 64 | impbid1 225 |
1
⊢ (𝐴 ∈ On →
((cf‘𝐴) = ∅
↔ 𝐴 =
∅)) |