| Step | Hyp | Ref
| Expression |
| 1 | | r1funlim 9806 |
. . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
| 2 | 1 | simpri 485 |
. . . . . 6
⊢ Lim dom
𝑅1 |
| 3 | | limord 6444 |
. . . . . 6
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
| 4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ Ord dom
𝑅1 |
| 5 | | ordsson 7803 |
. . . . 5
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
| 6 | 4, 5 | ax-mp 5 |
. . . 4
⊢ dom
𝑅1 ⊆ On |
| 7 | | elfvdm 6943 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ dom
𝑅1) |
| 8 | 6, 7 | sselid 3981 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ On) |
| 9 | | onzsl 7867 |
. . 3
⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵))) |
| 10 | 8, 9 | sylib 218 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵))) |
| 11 | | noel 4338 |
. . . . 5
⊢ ¬
𝐴 ∈
∅ |
| 12 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝐵 = ∅ →
(𝑅1‘𝐵) =
(𝑅1‘∅)) |
| 13 | | r10 9808 |
. . . . . . . 8
⊢
(𝑅1‘∅) = ∅ |
| 14 | 12, 13 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝐵 = ∅ →
(𝑅1‘𝐵) = ∅) |
| 15 | 14 | eleq2d 2827 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝐴 ∈ ∅)) |
| 16 | 15 | biimpcd 249 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ → 𝐴 ∈ ∅)) |
| 17 | 11, 16 | mtoi 199 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ¬ 𝐵 = ∅) |
| 18 | 17 | pm2.21d 121 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ → 𝒫 𝐴 ⊆
(𝑅1‘𝐵))) |
| 19 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ (𝑅1‘𝐵)) |
| 20 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 = suc 𝑥) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) =
(𝑅1‘suc 𝑥)) |
| 22 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom
𝑅1) |
| 23 | 20, 22 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) |
| 24 | | limsuc 7870 |
. . . . . . . . . . . 12
⊢ (Lim dom
𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc
𝑥 ∈ dom
𝑅1)) |
| 25 | 2, 24 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ dom
𝑅1 ↔ suc 𝑥 ∈ dom
𝑅1) |
| 26 | 23, 25 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝑥 ∈ dom
𝑅1) |
| 27 | | r1sucg 9809 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
| 29 | 21, 28 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫
(𝑅1‘𝑥)) |
| 30 | 19, 29 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫
(𝑅1‘𝑥)) |
| 31 | | elpwi 4607 |
. . . . . . 7
⊢ (𝐴 ∈ 𝒫
(𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥)) |
| 32 | | sspw 4611 |
. . . . . . 7
⊢ (𝐴 ⊆
(𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
| 33 | 30, 31, 32 | 3syl 18 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
| 34 | 33, 29 | sseqtrrd 4021 |
. . . . 5
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |
| 35 | 34 | ex 412 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
| 36 | 35 | rexlimdvw 3160 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
| 37 | | r1tr 9816 |
. . . . . 6
⊢ Tr
(𝑅1‘𝐵) |
| 38 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵)) |
| 39 | | r1limg 9811 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ dom
𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
| 40 | 7, 39 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
| 41 | 38, 40 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪
𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
| 42 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥)) |
| 43 | 41, 42 | sylib 218 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥)) |
| 44 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵) |
| 45 | | limsuc 7870 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵)) |
| 46 | 45 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵)) |
| 47 | 44, 46 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵) |
| 48 | | limsuc 7870 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵)) |
| 49 | 48 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵)) |
| 50 | 47, 49 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc suc 𝑥 ∈ 𝐵) |
| 51 | | r1tr 9816 |
. . . . . . . . . . . . . . 15
⊢ Tr
(𝑅1‘𝑥) |
| 52 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥)) |
| 53 | | trss 5270 |
. . . . . . . . . . . . . . 15
⊢ (Tr
(𝑅1‘𝑥) → (𝐴 ∈ (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))) |
| 54 | 51, 52, 53 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ⊆ (𝑅1‘𝑥)) |
| 55 | 54, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
| 56 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐵 ∈ dom
𝑅1) |
| 57 | | ordtr1 6427 |
. . . . . . . . . . . . . . . 16
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
| 58 | 4, 57 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1) |
| 59 | 44, 56, 58 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ dom
𝑅1) |
| 60 | 59, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) →
(𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
| 61 | 55, 60 | sseqtrrd 4021 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆
(𝑅1‘suc 𝑥)) |
| 62 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(𝑅1‘suc 𝑥) ∈ V |
| 63 | 62 | elpw2 5334 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc 𝑥) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
𝑥)) |
| 64 | 61, 63 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ 𝒫
(𝑅1‘suc 𝑥)) |
| 65 | 59, 25 | sylib 218 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ dom
𝑅1) |
| 66 | | r1sucg 9809 |
. . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ dom
𝑅1 → (𝑅1‘suc suc 𝑥) = 𝒫
(𝑅1‘suc 𝑥)) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) →
(𝑅1‘suc suc 𝑥) = 𝒫
(𝑅1‘suc 𝑥)) |
| 68 | 64, 67 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈
(𝑅1‘suc suc 𝑥)) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) =
(𝑅1‘suc suc 𝑥)) |
| 70 | 69 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈
(𝑅1‘suc suc 𝑥))) |
| 71 | 70 | rspcev 3622 |
. . . . . . . . . 10
⊢ ((suc suc
𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
| 72 | 50, 68, 71 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
| 73 | 43, 72 | rexlimddv 3161 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
| 74 | | eliun 4995 |
. . . . . . . 8
⊢
(𝒫 𝐴 ∈
∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
| 75 | 73, 74 | sylibr 234 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪
𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
| 76 | | r1limg 9811 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom
𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
| 77 | 7, 76 | sylan 580 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
| 78 | 75, 77 | eleqtrrd 2844 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵)) |
| 79 | | trss 5270 |
. . . . . 6
⊢ (Tr
(𝑅1‘𝐵) → (𝒫 𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆
(𝑅1‘𝐵))) |
| 80 | 37, 78, 79 | mpsyl 68 |
. . . . 5
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |
| 81 | 80 | ex 412 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (Lim 𝐵 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
| 82 | 81 | adantld 490 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ((𝐵 ∈ V ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
| 83 | 18, 36, 82 | 3jaod 1431 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
| 84 | 10, 83 | mpd 15 |
1
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |