Step | Hyp | Ref
| Expression |
1 | | r1funlim 9046 |
. . . . . . 7
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
2 | 1 | simpri 486 |
. . . . . 6
⊢ Lim dom
𝑅1 |
3 | | limord 6130 |
. . . . . 6
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ Ord dom
𝑅1 |
5 | | ordsson 7365 |
. . . . 5
⊢ (Ord dom
𝑅1 → dom 𝑅1 ⊆
On) |
6 | 4, 5 | ax-mp 5 |
. . . 4
⊢ dom
𝑅1 ⊆ On |
7 | | elfvdm 6575 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ dom
𝑅1) |
8 | 6, 7 | sseldi 3891 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝐵 ∈ On) |
9 | | onzsl 7422 |
. . 3
⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵))) |
10 | 8, 9 | sylib 219 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵))) |
11 | | noel 4220 |
. . . . 5
⊢ ¬
𝐴 ∈
∅ |
12 | | fveq2 6543 |
. . . . . . . 8
⊢ (𝐵 = ∅ →
(𝑅1‘𝐵) =
(𝑅1‘∅)) |
13 | | r10 9048 |
. . . . . . . 8
⊢
(𝑅1‘∅) = ∅ |
14 | 12, 13 | syl6eq 2847 |
. . . . . . 7
⊢ (𝐵 = ∅ →
(𝑅1‘𝐵) = ∅) |
15 | 14 | eleq2d 2868 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ∈
(𝑅1‘𝐵) ↔ 𝐴 ∈ ∅)) |
16 | 15 | biimpcd 250 |
. . . . 5
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ → 𝐴 ∈ ∅)) |
17 | 11, 16 | mtoi 200 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ¬ 𝐵 = ∅) |
18 | 17 | pm2.21d 121 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = ∅ → 𝒫 𝐴 ⊆
(𝑅1‘𝐵))) |
19 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ (𝑅1‘𝐵)) |
20 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 = suc 𝑥) |
21 | 20 | fveq2d 6547 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) =
(𝑅1‘suc 𝑥)) |
22 | 7 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom
𝑅1) |
23 | 20, 22 | eqeltrrd 2884 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom
𝑅1) |
24 | | limsuc 7425 |
. . . . . . . . . . . 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 235 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝑥 ∈ dom
𝑅1) |
27 | | r1sucg 9049 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom
𝑅1 → (𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc
𝑥) = 𝒫
(𝑅1‘𝑥)) |
29 | 21, 28 | eqtrd 2831 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫
(𝑅1‘𝑥)) |
30 | 19, 29 | eleqtrd 2885 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫
(𝑅1‘𝑥)) |
31 | | elpwi 4467 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝒫
(𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥)) |
32 | | sspwb 5238 |
. . . . . . . 8
⊢ (𝐴 ⊆
(𝑅1‘𝑥) ↔ 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
33 | 31, 32 | sylib 219 |
. . . . . . 7
⊢ (𝐴 ∈ 𝒫
(𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
34 | 30, 33 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
35 | 34, 29 | sseqtr4d 3933 |
. . . . 5
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |
36 | 35 | ex 413 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
37 | 36 | rexlimdvw 3253 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
38 | | r1tr 9056 |
. . . . . 6
⊢ Tr
(𝑅1‘𝐵) |
39 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵)) |
40 | | r1limg 9051 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ dom
𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
41 | 7, 40 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
42 | 39, 41 | eleqtrd 2885 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪
𝑥 ∈ 𝐵 (𝑅1‘𝑥)) |
43 | | eliun 4833 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥)) |
44 | 42, 43 | sylib 219 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥)) |
45 | | simprl 767 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵) |
46 | | limsuc 7425 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵)) |
47 | 46 | ad2antlr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵)) |
48 | 45, 47 | mpbid 233 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵) |
49 | | limsuc 7425 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵)) |
50 | 49 | ad2antlr 723 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵)) |
51 | 48, 50 | mpbid 233 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc suc 𝑥 ∈ 𝐵) |
52 | | r1tr 9056 |
. . . . . . . . . . . . . . 15
⊢ Tr
(𝑅1‘𝑥) |
53 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥)) |
54 | | trss 5077 |
. . . . . . . . . . . . . . 15
⊢ (Tr
(𝑅1‘𝑥) → (𝐴 ∈ (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))) |
55 | 52, 53, 54 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ⊆ (𝑅1‘𝑥)) |
56 | 55, 32 | sylib 219 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ 𝒫
(𝑅1‘𝑥)) |
57 | 7 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐵 ∈ dom
𝑅1) |
58 | | ordtr1 6114 |
. . . . . . . . . . . . . . . 16
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
59 | 4, 58 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1) |
60 | 45, 57, 59 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ dom
𝑅1) |
61 | 60, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) →
(𝑅1‘suc 𝑥) = 𝒫
(𝑅1‘𝑥)) |
62 | 56, 61 | sseqtr4d 3933 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆
(𝑅1‘suc 𝑥)) |
63 | | fvex 6556 |
. . . . . . . . . . . . 13
⊢
(𝑅1‘suc 𝑥) ∈ V |
64 | 63 | elpw2 5144 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∈
𝒫 (𝑅1‘suc 𝑥) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc
𝑥)) |
65 | 62, 64 | sylibr 235 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ 𝒫
(𝑅1‘suc 𝑥)) |
66 | 60, 25 | sylib 219 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ dom
𝑅1) |
67 | | r1sucg 9049 |
. . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ dom
𝑅1 → (𝑅1‘suc suc 𝑥) = 𝒫
(𝑅1‘suc 𝑥)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) →
(𝑅1‘suc suc 𝑥) = 𝒫
(𝑅1‘suc 𝑥)) |
69 | 65, 68 | eleqtrrd 2886 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈
(𝑅1‘suc suc 𝑥)) |
70 | | fveq2 6543 |
. . . . . . . . . . . 12
⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) =
(𝑅1‘suc suc 𝑥)) |
71 | 70 | eleq2d 2868 |
. . . . . . . . . . 11
⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈
(𝑅1‘suc suc 𝑥))) |
72 | 71 | rspcev 3559 |
. . . . . . . . . 10
⊢ ((suc suc
𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc
𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
73 | 51, 69, 72 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
74 | 44, 73 | rexlimddv 3254 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
75 | | eliun 4833 |
. . . . . . . 8
⊢
(𝒫 𝐴 ∈
∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦)) |
76 | 74, 75 | sylibr 235 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪
𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
77 | | r1limg 9051 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom
𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
78 | 7, 77 | sylan 580 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦)) |
79 | 76, 78 | eleqtrrd 2886 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵)) |
80 | | trss 5077 |
. . . . . 6
⊢ (Tr
(𝑅1‘𝐵) → (𝒫 𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆
(𝑅1‘𝐵))) |
81 | 38, 79, 80 | mpsyl 68 |
. . . . 5
⊢ ((𝐴 ∈
(𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |
82 | 81 | ex 413 |
. . . 4
⊢ (𝐴 ∈
(𝑅1‘𝐵) → (Lim 𝐵 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
83 | 82 | adantld 491 |
. . 3
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ((𝐵 ∈ V ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
84 | 18, 37, 83 | 3jaod 1421 |
. 2
⊢ (𝐴 ∈
(𝑅1‘𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))) |
85 | 10, 84 | mpd 15 |
1
⊢ (𝐴 ∈
(𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)) |