| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eltrpred |
⊢ ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) |
| 2 |
|
nn0suc |
⊢ ( 𝑖 ∈ ω → ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) ) |
| 3 |
|
fveq2 |
⊢ ( 𝑖 = ∅ → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ) |
| 4 |
3
|
eleq2d |
⊢ ( 𝑖 = ∅ → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ↔ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ) ) |
| 5 |
4
|
anbi2d |
⊢ ( 𝑖 = ∅ → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ) ) ) |
| 6 |
5
|
biimpd |
⊢ ( 𝑖 = ∅ → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ) ) ) |
| 7 |
|
setlikespec |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V ) |
| 8 |
|
fr0g |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) |
| 9 |
7 8
|
syl |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) ) |
| 10 |
9
|
eleq2d |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ↔ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) |
| 11 |
10
|
biimpa |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ) → 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) |
| 12 |
6 11
|
syl6com |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( 𝑖 = ∅ → 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) |
| 13 |
|
fveq2 |
⊢ ( 𝑖 = suc 𝑗 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) |
| 14 |
13
|
eleq2d |
⊢ ( 𝑖 = suc 𝑗 → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ↔ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) ) |
| 15 |
14
|
anbi2d |
⊢ ( 𝑖 = suc 𝑗 → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) ) ) |
| 16 |
15
|
biimpd |
⊢ ( 𝑖 = suc 𝑗 → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) ) ) |
| 17 |
|
fvex |
⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ∈ V |
| 18 |
|
trpredlem1 |
⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐴 ) |
| 19 |
7 18
|
syl |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐴 ) |
| 20 |
19
|
sseld |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → 𝑧 ∈ 𝐴 ) ) |
| 21 |
|
setlikespec |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
| 22 |
21
|
expcom |
⊢ ( 𝑅 Se 𝐴 → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) ) |
| 23 |
22
|
adantl |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) ) |
| 24 |
20 23
|
syld |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) ) |
| 25 |
24
|
ralrimiv |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
| 26 |
|
iunexg |
⊢ ( ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ∈ V ∧ ∀ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) → ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
| 27 |
17 25 26
|
sylancr |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) |
| 28 |
|
nfcv |
⊢ Ⅎ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑋 ) |
| 29 |
|
nfcv |
⊢ Ⅎ 𝑎 𝑗 |
| 30 |
|
nfmpt1 |
⊢ Ⅎ 𝑎 ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) |
| 31 |
30 28
|
nfrdg |
⊢ Ⅎ 𝑎 rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) |
| 32 |
|
nfcv |
⊢ Ⅎ 𝑎 ω |
| 33 |
31 32
|
nfres |
⊢ Ⅎ 𝑎 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) |
| 34 |
33 29
|
nffv |
⊢ Ⅎ 𝑎 ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) |
| 35 |
|
nfcv |
⊢ Ⅎ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) |
| 36 |
34 35
|
nfiun |
⊢ Ⅎ 𝑎 ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) |
| 37 |
|
eqid |
⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) |
| 38 |
|
predeq3 |
⊢ ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 39 |
38
|
cbviunv |
⊢ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) |
| 40 |
|
iuneq1 |
⊢ ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → ∪ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) = ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 41 |
39 40
|
syl5eq |
⊢ ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 42 |
28 29 36 37 41
|
frsucmpt |
⊢ ( ( 𝑗 ∈ ω ∧ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) = ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 43 |
27 42
|
sylan2 |
⊢ ( ( 𝑗 ∈ ω ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) = ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 44 |
43
|
eleq2d |
⊢ ( ( 𝑗 ∈ ω ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ) → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ↔ 𝑌 ∈ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
| 45 |
44
|
biimpd |
⊢ ( ( 𝑗 ∈ ω ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ) → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) → 𝑌 ∈ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
| 46 |
45
|
expimpd |
⊢ ( 𝑗 ∈ ω → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) → 𝑌 ∈ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) |
| 47 |
|
eliun |
⊢ ( 𝑌 ∈ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ↔ ∃ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) |
| 48 |
|
ssiun2 |
⊢ ( 𝑗 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ ∪ 𝑗 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ) |
| 49 |
|
dftrpred2 |
⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑗 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) |
| 50 |
48 49
|
sseqtrrdi |
⊢ ( 𝑗 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) |
| 51 |
50
|
sseld |
⊢ ( 𝑗 ∈ ω → ( 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) ) |
| 52 |
|
vex |
⊢ 𝑧 ∈ V |
| 53 |
52
|
elpredim |
⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → 𝑌 𝑅 𝑧 ) |
| 54 |
53
|
a1i |
⊢ ( 𝑗 ∈ ω → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → 𝑌 𝑅 𝑧 ) ) |
| 55 |
51 54
|
anim12d |
⊢ ( 𝑗 ∈ ω → ( ( 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 𝑅 𝑧 ) ) ) |
| 56 |
55
|
reximdv2 |
⊢ ( 𝑗 ∈ ω → ( ∃ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) |
| 57 |
56
|
com12 |
⊢ ( ∃ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → ( 𝑗 ∈ ω → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) |
| 58 |
47 57
|
sylbi |
⊢ ( 𝑌 ∈ ∪ 𝑧 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) → ( 𝑗 ∈ ω → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) |
| 59 |
46 58
|
syl6com |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) → ( 𝑗 ∈ ω → ( 𝑗 ∈ ω → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |
| 60 |
59
|
pm2.43d |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ) → ( 𝑗 ∈ ω → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) |
| 61 |
16 60
|
syl6com |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( 𝑖 = suc 𝑗 → ( 𝑗 ∈ ω → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |
| 62 |
61
|
com23 |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( 𝑗 ∈ ω → ( 𝑖 = suc 𝑗 → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |
| 63 |
62
|
rexlimdv |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 → ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) |
| 64 |
12 63
|
orim12d |
⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |
| 65 |
64
|
ex |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → ( ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) ) |
| 66 |
65
|
com23 |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) ) |
| 67 |
2 66
|
syl5 |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑖 ∈ ω → ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) ) |
| 68 |
67
|
rexlimdv |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |
| 69 |
1 68
|
syl5bi |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ ∃ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) 𝑌 𝑅 𝑧 ) ) ) |