Step |
Hyp |
Ref |
Expression |
1 |
|
df-trpred |
⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) |
2 |
|
frfnom |
⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω |
3 |
|
fniunfv |
⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω → ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ) |
4 |
2 3
|
ax-mp |
⊢ ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ∪ ran ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) |
5 |
1 4
|
eqtr4i |
⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) |