| Step | Hyp | Ref
| Expression |
| 1 | | rankwflemb 9833 |
. . . 4
⊢ (𝑦 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑧 ∈ On 𝑦 ∈ (𝑅1‘suc
𝑧)) |
| 2 | | harcl 9599 |
. . . . . . . . 9
⊢
(har‘(𝑅1‘𝑧)) ∈ On |
| 3 | | pweq 4614 |
. . . . . . . . . . 11
⊢ (𝑥 =
(har‘(𝑅1‘𝑧)) → 𝒫 𝑥 = 𝒫
(har‘(𝑅1‘𝑧))) |
| 4 | 3 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 =
(har‘(𝑅1‘𝑧)) → (𝒫 𝑥 ∈ dom card ↔ 𝒫
(har‘(𝑅1‘𝑧)) ∈ dom card)) |
| 5 | 4 | rspcv 3618 |
. . . . . . . . 9
⊢
((har‘(𝑅1‘𝑧)) ∈ On → (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card →
𝒫 (har‘(𝑅1‘𝑧)) ∈ dom card)) |
| 6 | 2, 5 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ 𝒫 (har‘(𝑅1‘𝑧)) ∈ dom card) |
| 7 | | cardid2 9993 |
. . . . . . . 8
⊢
(𝒫 (har‘(𝑅1‘𝑧)) ∈ dom card →
(card‘𝒫 (har‘(𝑅1‘𝑧))) ≈ 𝒫
(har‘(𝑅1‘𝑧))) |
| 8 | | ensym 9043 |
. . . . . . . 8
⊢
((card‘𝒫 (har‘(𝑅1‘𝑧))) ≈ 𝒫
(har‘(𝑅1‘𝑧)) → 𝒫
(har‘(𝑅1‘𝑧)) ≈ (card‘𝒫
(har‘(𝑅1‘𝑧)))) |
| 9 | | bren 8995 |
. . . . . . . . 9
⊢
(𝒫 (har‘(𝑅1‘𝑧)) ≈ (card‘𝒫
(har‘(𝑅1‘𝑧))) ↔ ∃𝑓 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧)))) |
| 10 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) ∧ 𝑧 ∈ On) → 𝑧 ∈ On) |
| 11 | | f1of1 6847 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) → 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1→(card‘𝒫
(har‘(𝑅1‘𝑧)))) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) ∧ 𝑧 ∈ On) → 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1→(card‘𝒫
(har‘(𝑅1‘𝑧)))) |
| 13 | | cardon 9984 |
. . . . . . . . . . . . . 14
⊢
(card‘𝒫 (har‘(𝑅1‘𝑧))) ∈ On |
| 14 | 13 | onssi 7858 |
. . . . . . . . . . . . 13
⊢
(card‘𝒫 (har‘(𝑅1‘𝑧))) ⊆ On |
| 15 | | f1ss 6809 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1→(card‘𝒫
(har‘(𝑅1‘𝑧))) ∧ (card‘𝒫
(har‘(𝑅1‘𝑧))) ⊆ On) → 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1→On) |
| 16 | 12, 14, 15 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) ∧ 𝑧 ∈ On) → 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1→On) |
| 17 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑏 → (rank‘𝑦) = (rank‘𝑏)) |
| 18 | 17 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑏 → (suc ∪ ran
∪ ran 𝑥 ·o (rank‘𝑦)) = (suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑏))) |
| 19 | | suceq 6450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((rank‘𝑦) =
(rank‘𝑏) → suc
(rank‘𝑦) = suc
(rank‘𝑏)) |
| 20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑏 → suc (rank‘𝑦) = suc (rank‘𝑏)) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑏 → (𝑥‘suc (rank‘𝑦)) = (𝑥‘suc (rank‘𝑏))) |
| 22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑏 → 𝑦 = 𝑏) |
| 23 | 21, 22 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑏 → ((𝑥‘suc (rank‘𝑦))‘𝑦) = ((𝑥‘suc (rank‘𝑏))‘𝑏)) |
| 24 | 18, 23 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑏 → ((suc ∪
ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)) = ((suc ∪ ran
∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏))) |
| 25 | | imaeq2 6074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑏 → ((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦) = ((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏)) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑏 → (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)) = (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏))) |
| 27 | 24, 26 | ifeq12d 4547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑏 → if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦))) = if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏)))) |
| 28 | 27 | cbvmptv 5255 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈
(𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))) = (𝑏 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏)))) |
| 29 | | dmeq 5914 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → dom 𝑥 = dom 𝑎) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑅1‘dom
𝑥) =
(𝑅1‘dom 𝑎)) |
| 31 | 29 | unieqd 4920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ∪ dom
𝑥 = ∪ dom 𝑎) |
| 32 | 29, 31 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (dom 𝑥 = ∪ dom 𝑥 ↔ dom 𝑎 = ∪ dom 𝑎)) |
| 33 | | rneq 5947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → ran 𝑥 = ran 𝑎) |
| 34 | 33 | unieqd 4920 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑎 → ∪ ran
𝑥 = ∪ ran 𝑎) |
| 35 | 34 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → ran ∪ ran
𝑥 = ran ∪ ran 𝑎) |
| 36 | 35 | unieqd 4920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → ∪ ran
∪ ran 𝑥 = ∪ ran ∪ ran 𝑎) |
| 37 | | suceq 6450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∪ ran ∪ ran 𝑥 = ∪ ran ∪ ran 𝑎 → suc ∪ ran
∪ ran 𝑥 = suc ∪ ran ∪ ran 𝑎) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → suc ∪ ran
∪ ran 𝑥 = suc ∪ ran ∪ ran 𝑎) |
| 39 | 38 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (suc ∪ ran
∪ ran 𝑥 ·o (rank‘𝑏)) = (suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏))) |
| 40 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝑥‘suc (rank‘𝑏)) = (𝑎‘suc (rank‘𝑏))) |
| 41 | 40 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝑥‘suc (rank‘𝑏))‘𝑏) = ((𝑎‘suc (rank‘𝑏))‘𝑏)) |
| 42 | 39, 41 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → ((suc ∪
ran ∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏)) = ((suc ∪ ran
∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏))) |
| 43 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎) |
| 44 | 43, 31 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → (𝑥‘∪ dom 𝑥) = (𝑎‘∪ dom 𝑎)) |
| 45 | 44 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑎 → ran (𝑥‘∪ dom 𝑥) = ran (𝑎‘∪ dom 𝑎)) |
| 46 | | oieq2 9553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ran
(𝑥‘∪ dom 𝑥) = ran (𝑎‘∪ dom 𝑎) → OrdIso( E , ran (𝑥‘∪ dom 𝑥)) = OrdIso( E , ran (𝑎‘∪ dom 𝑎))) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → OrdIso( E , ran (𝑥‘∪ dom 𝑥)) = OrdIso( E , ran (𝑎‘∪ dom 𝑎))) |
| 48 | 47 | cnveqd 5886 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → ◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) = ◡OrdIso( E , ran (𝑎‘∪ dom 𝑎))) |
| 49 | 48, 44 | coeq12d 5875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) = (◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎))) |
| 50 | 49 | imaeq1d 6077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏) = ((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏)) |
| 51 | 50 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏)) = (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))) |
| 52 | 32, 42, 51 | ifbieq12d 4554 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏))) = if(dom 𝑎 = ∪ dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏)))) |
| 53 | 30, 52 | mpteq12dv 5233 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝑏 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑏)) +o ((𝑥‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑏)))) = (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))))) |
| 54 | 28, 53 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑦 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))) = (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))))) |
| 55 | 54 | cbvmptv 5255 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V ↦ (𝑦 ∈
(𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦))))) = (𝑎 ∈ V ↦ (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))))) |
| 56 | | recseq 8414 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ V ↦ (𝑦 ∈
(𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦))))) = (𝑎 ∈ V ↦ (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))))) → recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom
𝑥) ↦ if(dom 𝑥 = ∪
dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) = recs((𝑎 ∈ V ↦ (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏))))))) |
| 57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
recs((𝑥 ∈ V
↦ (𝑦 ∈
(𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝑓‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) = recs((𝑎 ∈ V ↦ (𝑏 ∈ (𝑅1‘dom
𝑎) ↦ if(dom 𝑎 = ∪
dom 𝑎, ((suc ∪ ran ∪ ran 𝑎 ·o (rank‘𝑏)) +o ((𝑎‘suc (rank‘𝑏))‘𝑏)), (𝑓‘((◡OrdIso( E , ran (𝑎‘∪ dom 𝑎)) ∘ (𝑎‘∪ dom 𝑎)) “ 𝑏)))))) |
| 58 | 10, 16, 57 | dfac12lem3 10186 |
. . . . . . . . . . 11
⊢ ((𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) ∧ 𝑧 ∈ On) →
(𝑅1‘𝑧) ∈ dom card) |
| 59 | 58 | ex 412 |
. . . . . . . . . 10
⊢ (𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) → (𝑧 ∈ On →
(𝑅1‘𝑧) ∈ dom card)) |
| 60 | 59 | exlimiv 1930 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓:𝒫
(har‘(𝑅1‘𝑧))–1-1-onto→(card‘𝒫
(har‘(𝑅1‘𝑧))) → (𝑧 ∈ On →
(𝑅1‘𝑧) ∈ dom card)) |
| 61 | 9, 60 | sylbi 217 |
. . . . . . . 8
⊢
(𝒫 (har‘(𝑅1‘𝑧)) ≈ (card‘𝒫
(har‘(𝑅1‘𝑧))) → (𝑧 ∈ On →
(𝑅1‘𝑧) ∈ dom card)) |
| 62 | 6, 7, 8, 61 | 4syl 19 |
. . . . . . 7
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ (𝑧 ∈ On →
(𝑅1‘𝑧) ∈ dom card)) |
| 63 | 62 | imp 406 |
. . . . . 6
⊢
((∀𝑥 ∈
On 𝒫 𝑥 ∈ dom
card ∧ 𝑧 ∈ On)
→ (𝑅1‘𝑧) ∈ dom card) |
| 64 | | r1suc 9810 |
. . . . . . . . 9
⊢ (𝑧 ∈ On →
(𝑅1‘suc 𝑧) = 𝒫
(𝑅1‘𝑧)) |
| 65 | 64 | adantl 481 |
. . . . . . . 8
⊢
((∀𝑥 ∈
On 𝒫 𝑥 ∈ dom
card ∧ 𝑧 ∈ On)
→ (𝑅1‘suc 𝑧) = 𝒫
(𝑅1‘𝑧)) |
| 66 | 65 | eleq2d 2827 |
. . . . . . 7
⊢
((∀𝑥 ∈
On 𝒫 𝑥 ∈ dom
card ∧ 𝑧 ∈ On)
→ (𝑦 ∈
(𝑅1‘suc 𝑧) ↔ 𝑦 ∈ 𝒫
(𝑅1‘𝑧))) |
| 67 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫
(𝑅1‘𝑧) → 𝑦 ⊆ (𝑅1‘𝑧)) |
| 68 | 66, 67 | biimtrdi 253 |
. . . . . 6
⊢
((∀𝑥 ∈
On 𝒫 𝑥 ∈ dom
card ∧ 𝑧 ∈ On)
→ (𝑦 ∈
(𝑅1‘suc 𝑧) → 𝑦 ⊆ (𝑅1‘𝑧))) |
| 69 | | ssnum 10079 |
. . . . . 6
⊢
(((𝑅1‘𝑧) ∈ dom card ∧ 𝑦 ⊆ (𝑅1‘𝑧)) → 𝑦 ∈ dom card) |
| 70 | 63, 68, 69 | syl6an 684 |
. . . . 5
⊢
((∀𝑥 ∈
On 𝒫 𝑥 ∈ dom
card ∧ 𝑧 ∈ On)
→ (𝑦 ∈
(𝑅1‘suc 𝑧) → 𝑦 ∈ dom card)) |
| 71 | 70 | rexlimdva 3155 |
. . . 4
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ (∃𝑧 ∈ On
𝑦 ∈
(𝑅1‘suc 𝑧) → 𝑦 ∈ dom card)) |
| 72 | 1, 71 | biimtrid 242 |
. . 3
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ (𝑦 ∈ ∪ (𝑅1 “ On) → 𝑦 ∈ dom
card)) |
| 73 | 72 | ssrdv 3989 |
. 2
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
→ ∪ (𝑅1 “ On) ⊆
dom card) |
| 74 | | onwf 9870 |
. . . . . 6
⊢ On
⊆ ∪ (𝑅1 “
On) |
| 75 | 74 | sseli 3979 |
. . . . 5
⊢ (𝑥 ∈ On → 𝑥 ∈ ∪ (𝑅1 “ On)) |
| 76 | | pwwf 9847 |
. . . . 5
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ 𝒫
𝑥 ∈ ∪ (𝑅1 “ On)) |
| 77 | 75, 76 | sylib 218 |
. . . 4
⊢ (𝑥 ∈ On → 𝒫
𝑥 ∈ ∪ (𝑅1 “ On)) |
| 78 | | ssel 3977 |
. . . 4
⊢ (∪ (𝑅1 “ On) ⊆ dom card
→ (𝒫 𝑥 ∈
∪ (𝑅1 “ On) →
𝒫 𝑥 ∈ dom
card)) |
| 79 | 77, 78 | syl5 34 |
. . 3
⊢ (∪ (𝑅1 “ On) ⊆ dom card
→ (𝑥 ∈ On →
𝒫 𝑥 ∈ dom
card)) |
| 80 | 79 | ralrimiv 3145 |
. 2
⊢ (∪ (𝑅1 “ On) ⊆ dom card
→ ∀𝑥 ∈ On
𝒫 𝑥 ∈ dom
card) |
| 81 | 73, 80 | impbii 209 |
1
⊢
(∀𝑥 ∈ On
𝒫 𝑥 ∈ dom card
↔ ∪ (𝑅1 “ On) ⊆
dom card) |