Step | Hyp | Ref
| Expression |
1 | | eltrpred 9331 |
. 2
⊢ (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) ↔ ∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) |
2 | | nn0suc 7673 |
. . . 4
⊢ (𝑖 ∈ ω → (𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗)) |
3 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑖 = ∅ → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾
ω)‘∅)) |
4 | 3 | eleq2d 2823 |
. . . . . . . . . 10
⊢ (𝑖 = ∅ → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ↔ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾
ω)‘∅))) |
5 | 4 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑖 = ∅ → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾
ω)‘∅)))) |
6 | 5 | biimpd 232 |
. . . . . . . 8
⊢ (𝑖 = ∅ → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾
ω)‘∅)))) |
7 | | setlikespec 6183 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V) |
8 | | fr0g 8171 |
. . . . . . . . . . 11
⊢
(Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) =
Pred(𝑅, 𝐴, 𝑋)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) =
Pred(𝑅, 𝐴, 𝑋)) |
10 | 9 | eleq2d 2823 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅) ↔
𝑌 ∈ Pred(𝑅, 𝐴, 𝑋))) |
11 | 10 | biimpa 480 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘∅)) →
𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) |
12 | 6, 11 | syl6com 37 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑖 = ∅ → 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋))) |
13 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑖 = suc 𝑗 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) |
14 | 13 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢ (𝑖 = suc 𝑗 → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ↔ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗))) |
15 | 14 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝑖 = suc 𝑗 → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)))) |
16 | 15 | biimpd 232 |
. . . . . . . . . 10
⊢ (𝑖 = suc 𝑗 → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)))) |
17 | | fvex 6730 |
. . . . . . . . . . . . . . . . 17
⊢
((rec((𝑎 ∈ V
↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∈ V |
18 | | trpredlem1 9332 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Pred(𝑅, 𝐴, 𝑋) ∈ V → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐴) |
19 | 7, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ 𝐴) |
20 | 19 | sseld 3900 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → 𝑧 ∈ 𝐴)) |
21 | | setlikespec 6183 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑧) ∈ V) |
22 | 21 | expcom 417 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 Se 𝐴 → (𝑧 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑧) ∈ V)) |
23 | 22 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑧) ∈ V)) |
24 | 20, 23 | syld 47 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → Pred(𝑅, 𝐴, 𝑧) ∈ V)) |
25 | 24 | ralrimiv 3104 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) |
26 | | iunexg 7736 |
. . . . . . . . . . . . . . . . 17
⊢
((((rec((𝑎 ∈ V
↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∈ V ∧ ∀𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) |
27 | 17, 25, 26 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ∪
𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) |
28 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎Pred(𝑅, 𝐴, 𝑋) |
29 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎𝑗 |
30 | | nfmpt1 5153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎(𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)) |
31 | 30, 28 | nfrdg 8150 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) |
32 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎ω |
33 | 31, 32 | nfres 5853 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑎(rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) |
34 | 33, 29 | nffv 6727 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑎((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) |
35 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑎Pred(𝑅, 𝐴, 𝑧) |
36 | 34, 35 | nfiun 4934 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(rec((𝑎 ∈ V
↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) |
38 | | predeq3 6164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑧)) |
39 | 38 | cbviunv 4949 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑧 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑧) |
40 | | iuneq1 4920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → ∪
𝑧 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑧) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)) |
41 | 39, 40 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → ∪
𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)) |
42 | 28, 29, 36, 37, 41 | frsucmpt 8173 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ω ∧ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)) |
43 | 27, 42 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) = ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧)) |
44 | 43 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) ↔ 𝑌 ∈ ∪
𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))) |
45 | 44 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ω ∧ (𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴)) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗) → 𝑌 ∈ ∪
𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))) |
46 | 45 | expimpd 457 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ω → (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → 𝑌 ∈ ∪
𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧))) |
47 | | eliun 4908 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧)) |
48 | | ssiun2 4956 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ω →
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ ∪
𝑗 ∈ ω
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)) |
49 | | dftrpred2 9324 |
. . . . . . . . . . . . . . . . . 18
⊢
TrPred(𝑅, 𝐴, 𝑋) = ∪
𝑗 ∈ ω
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) |
50 | 48, 49 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ω →
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ⊆ TrPred(𝑅, 𝐴, 𝑋)) |
51 | 50 | sseld 3900 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ω → (𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) → 𝑧 ∈ TrPred(𝑅, 𝐴, 𝑋))) |
52 | | vex 3412 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
53 | 52 | elpredim 6175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → 𝑌𝑅𝑧) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ω → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → 𝑌𝑅𝑧)) |
55 | 51, 54 | anim12d 612 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ω → ((𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑧)) → (𝑧 ∈ TrPred(𝑅, 𝐴, 𝑋) ∧ 𝑌𝑅𝑧))) |
56 | 55 | reximdv2 3190 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ω →
(∃𝑧 ∈
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
((rec((𝑎 ∈ V ↦
∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)𝑌 ∈ Pred(𝑅, 𝐴, 𝑧) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)) |
58 | 47, 57 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ ∪ 𝑧 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑗)Pred(𝑅, 𝐴, 𝑧) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)) |
59 | 46, 58 | syl6com 37 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → (𝑗 ∈ ω → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |
60 | 59 | pm2.43d 53 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘suc 𝑗)) → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)) |
61 | 16, 60 | syl6com 37 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑖 = suc 𝑗 → (𝑗 ∈ ω → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |
62 | 61 | com23 86 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (𝑗 ∈ ω → (𝑖 = suc 𝑗 → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |
63 | 62 | rexlimdv 3202 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → (∃𝑗 ∈ ω 𝑖 = suc 𝑗 → ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)) |
64 | 12, 63 | orim12d 965 |
. . . . . 6
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |
65 | 64 | ex 416 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))) |
66 | 65 | com23 86 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → ((𝑖 = ∅ ∨ ∃𝑗 ∈ ω 𝑖 = suc 𝑗) → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))) |
67 | 2, 66 | syl5 34 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑖 ∈ ω → (𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧)))) |
68 | 67 | rexlimdv 3202 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |
69 | 1, 68 | syl5bi 245 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) |