| Step | Hyp | Ref
| Expression |
| 1 | | df-finxp 37385 |
. . 3
⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} |
| 2 | 1 | csbeq2i 3907 |
. 2
⊢
⦋𝐴 /
𝑥⦌(𝑈↑↑𝑁) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} |
| 3 | | sbcan 3838 |
. . . . 5
⊢
([𝐴 / 𝑥](𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁)) ↔ ([𝐴 / 𝑥]𝑁 ∈ ω ∧ [𝐴 / 𝑥]∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))) |
| 4 | | sbcel1g 4416 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑁 ∈ ω ↔ ⦋𝐴 / 𝑥⦌𝑁 ∈ ω)) |
| 5 | | sbceq2g 4419 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁) ↔ ∅ = ⦋𝐴 / 𝑥⦌(rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))) |
| 6 | | csbfv12 6954 |
. . . . . . . . 9
⊢
⦋𝐴 /
𝑥⦌(rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁) = (⦋𝐴 / 𝑥⦌rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁) |
| 7 | | csbrdgg 37330 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉) = rec(⦋𝐴 / 𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉)) |
| 8 | | csbmpo123 37332 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) = (𝑛 ∈ ⦋𝐴 / 𝑥⦌ω, 𝑧 ∈ ⦋𝐴 / 𝑥⦌V ↦ ⦋𝐴 / 𝑥⦌if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)))) |
| 9 | | csbconstg 3918 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ω =
ω) |
| 10 | | csbconstg 3918 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌V = V) |
| 11 | | csbif 4583 |
. . . . . . . . . . . . . . 15
⊢
⦋𝐴 /
𝑥⦌if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) = if([𝐴 / 𝑥](𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ⦋𝐴 / 𝑥⦌∅, ⦋𝐴 / 𝑥⦌if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) |
| 12 | | sbcan 3838 |
. . . . . . . . . . . . . . . . 17
⊢
([𝐴 / 𝑥](𝑛 = 1o ∧ 𝑧 ∈ 𝑈) ↔ ([𝐴 / 𝑥]𝑛 = 1o ∧ [𝐴 / 𝑥]𝑧 ∈ 𝑈)) |
| 13 | | sbcg 3863 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑛 = 1o ↔ 𝑛 = 1o)) |
| 14 | | sbcel12 4411 |
. . . . . . . . . . . . . . . . . . 19
⊢
([𝐴 / 𝑥]𝑧 ∈ 𝑈 ↔ ⦋𝐴 / 𝑥⦌𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈) |
| 15 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑧 = 𝑧) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈 ↔ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈)) |
| 17 | 14, 16 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈)) |
| 18 | 13, 17 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑛 = 1o ∧ [𝐴 / 𝑥]𝑧 ∈ 𝑈) ↔ (𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈))) |
| 19 | 12, 18 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑛 = 1o ∧ 𝑧 ∈ 𝑈) ↔ (𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈))) |
| 20 | | csbconstg 3918 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∅ =
∅) |
| 21 | | csbif 4583 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝐴 /
𝑥⦌if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑧)〉, 〈𝑛, 𝑧〉) = if([𝐴 / 𝑥]𝑧 ∈ (V × 𝑈), ⦋𝐴 / 𝑥⦌〈∪ 𝑛,
(1st ‘𝑧)〉, ⦋𝐴 / 𝑥⦌〈𝑛, 𝑧〉) |
| 22 | | sbcel12 4411 |
. . . . . . . . . . . . . . . . . . 19
⊢
([𝐴 / 𝑥]𝑧 ∈ (V × 𝑈) ↔ ⦋𝐴 / 𝑥⦌𝑧 ∈ ⦋𝐴 / 𝑥⦌(V × 𝑈)) |
| 23 | | csbxp 5785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋𝐴 /
𝑥⦌(V ×
𝑈) = (⦋𝐴 / 𝑥⦌V × ⦋𝐴 / 𝑥⦌𝑈) |
| 24 | 10 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌V × ⦋𝐴 / 𝑥⦌𝑈) = (V × ⦋𝐴 / 𝑥⦌𝑈)) |
| 25 | 23, 24 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(V × 𝑈) = (V × ⦋𝐴 / 𝑥⦌𝑈)) |
| 26 | 15, 25 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝑧 ∈ ⦋𝐴 / 𝑥⦌(V × 𝑈) ↔ 𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈))) |
| 27 | 22, 26 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ∈ (V × 𝑈) ↔ 𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈))) |
| 28 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈∪ 𝑛,
(1st ‘𝑧)〉 = 〈∪
𝑛, (1st
‘𝑧)〉) |
| 29 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝑛, 𝑧〉 = 〈𝑛, 𝑧〉) |
| 30 | 27, 28, 29 | ifbieq12d 4554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → if([𝐴 / 𝑥]𝑧 ∈ (V × 𝑈), ⦋𝐴 / 𝑥⦌〈∪ 𝑛,
(1st ‘𝑧)〉, ⦋𝐴 / 𝑥⦌〈𝑛, 𝑧〉) = if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) |
| 31 | 21, 30 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉) = if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) |
| 32 | 19, 20, 31 | ifbieq12d 4554 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → if([𝐴 / 𝑥](𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ⦋𝐴 / 𝑥⦌∅, ⦋𝐴 / 𝑥⦌if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) = if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) |
| 33 | 11, 32 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)) = if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) |
| 34 | 9, 10, 33 | mpoeq123dv 7508 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (𝑛 ∈ ⦋𝐴 / 𝑥⦌ω, 𝑧 ∈ ⦋𝐴 / 𝑥⦌V ↦ ⦋𝐴 / 𝑥⦌if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) = (𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)))) |
| 35 | 8, 34 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) = (𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉)))) |
| 36 | | csbopg 4891 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉 = 〈⦋𝐴 / 𝑥⦌𝑁, ⦋𝐴 / 𝑥⦌𝑦〉) |
| 37 | | csbconstg 3918 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦) |
| 38 | 37 | opeq2d 4880 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → 〈⦋𝐴 / 𝑥⦌𝑁, ⦋𝐴 / 𝑥⦌𝑦〉 = 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉) |
| 39 | 36, 38 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉 = 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉) |
| 40 | | rdgeq12 8453 |
. . . . . . . . . . . 12
⊢
((⦋𝐴 /
𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) = (𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))) ∧ ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉 = 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉) → rec(⦋𝐴 / 𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉) = rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)) |
| 41 | 35, 39, 40 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → rec(⦋𝐴 / 𝑥⦌(𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), ⦋𝐴 / 𝑥⦌〈𝑁, 𝑦〉) = rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)) |
| 42 | 7, 41 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉) = rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)) |
| 43 | 42 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁) = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁)) |
| 44 | 6, 43 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁) = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁)) |
| 45 | 44 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (∅ = ⦋𝐴 / 𝑥⦌(rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁) ↔ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁))) |
| 46 | 5, 45 | bitrd 279 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁) ↔ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁))) |
| 47 | 4, 46 | anbi12d 632 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑁 ∈ ω ∧ [𝐴 / 𝑥]∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁)) ↔ (⦋𝐴 / 𝑥⦌𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁)))) |
| 48 | 3, 47 | bitrid 283 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁)) ↔ (⦋𝐴 / 𝑥⦌𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁)))) |
| 49 | 48 | abbidv 2808 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ [𝐴 / 𝑥](𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁))}) |
| 50 | | csbab 4440 |
. . 3
⊢
⦋𝐴 /
𝑥⦌{𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} = {𝑦 ∣ [𝐴 / 𝑥](𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} |
| 51 | | df-finxp 37385 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌𝑈↑↑⦋𝐴 / 𝑥⦌𝑁) = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑈), ∅, if(𝑧 ∈ (V × ⦋𝐴 / 𝑥⦌𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈⦋𝐴 / 𝑥⦌𝑁, 𝑦〉)‘⦋𝐴 / 𝑥⦌𝑁))} |
| 52 | 49, 50, 51 | 3eqtr4g 2802 |
. 2
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑧 ∈ V ↦ if((𝑛 = 1o ∧ 𝑧 ∈ 𝑈), ∅, if(𝑧 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑧)〉, 〈𝑛, 𝑧〉))), 〈𝑁, 𝑦〉)‘𝑁))} = (⦋𝐴 / 𝑥⦌𝑈↑↑⦋𝐴 / 𝑥⦌𝑁)) |
| 53 | 2, 52 | eqtrid 2789 |
1
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑈↑↑𝑁) = (⦋𝐴 / 𝑥⦌𝑈↑↑⦋𝐴 / 𝑥⦌𝑁)) |