Step | Hyp | Ref
| Expression |
1 | | csbuni 4740 |
. . 3
⊢
⦋𝐴 /
𝑥⦌∪ {𝑓
∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = ∪
⦋𝐴 / 𝑥⦌{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} |
2 | | csbab 4273 |
. . . . 5
⊢
⦋𝐴 /
𝑥⦌{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ [𝐴 / 𝑥]∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} |
3 | | sbcex2 3738 |
. . . . . . 7
⊢
([𝐴 / 𝑥]∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧[𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))) |
4 | | sbc3an 3742 |
. . . . . . . . 9
⊢
([𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ([𝐴 / 𝑥]𝑓 Fn 𝑧 ∧ [𝐴 / 𝑥](𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ [𝐴 / 𝑥]∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))) |
5 | | sbcg 3751 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑓 Fn 𝑧 ↔ 𝑓 Fn 𝑧)) |
6 | | sbcan 3726 |
. . . . . . . . . . 11
⊢
([𝐴 / 𝑥](𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ ([𝐴 / 𝑥]𝑧 ⊆ 𝐷 ∧ [𝐴 / 𝑥]∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧)) |
7 | | sbcssg 4346 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ⊆ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) |
8 | | csbconstg 3800 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑧 = 𝑧) |
9 | 8 | sseq1d 3889 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ↔ 𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) |
10 | 7, 9 | bitrd 271 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑧 ⊆ 𝐷 ↔ 𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷)) |
11 | | sbcralg 3761 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦 ∈ 𝑧 [𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧)) |
12 | | sbcssg 4346 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) ⊆ ⦋𝐴 / 𝑥⦌𝑧)) |
13 | 8 | sseq2d 3890 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) ⊆ ⦋𝐴 / 𝑥⦌𝑧 ↔ ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧)) |
14 | | csbpredg 34046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑦)) |
15 | | csbconstg 3800 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦) |
16 | | predeq3 5990 |
. . . . . . . . . . . . . . . . . 18
⊢
(⦋𝐴 /
𝑥⦌𝑦 = 𝑦 → Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑦) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑦) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)) |
18 | 14, 17 | eqtrd 2815 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)) |
19 | 18 | sseq1d 3889 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧)) |
20 | 12, 13, 19 | 3bitrd 297 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧)) |
21 | 20 | ralbidv 3148 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝑧 [𝐴 / 𝑥]Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧)) |
22 | 11, 21 | bitrd 271 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧 ↔ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧)) |
23 | 10, 22 | anbi12d 621 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑧 ⊆ 𝐷 ∧ [𝐴 / 𝑥]∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧))) |
24 | 6, 23 | syl5bb 275 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ↔ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧))) |
25 | | sbcralg 3761 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦 ∈ 𝑧 [𝐴 / 𝑥](𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))) |
26 | | sbceqg 4247 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ⦋𝐴 / 𝑥⦌(𝑓‘𝑦) = ⦋𝐴 / 𝑥⦌(𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))) |
27 | | csbconstg 3800 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑓‘𝑦) = (𝑓‘𝑦)) |
28 | | csbfv12 6543 |
. . . . . . . . . . . . . . 15
⊢
⦋𝐴 /
𝑥⦌(𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) |
29 | | csbres 5698 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝐴 /
𝑥⦌(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)) = (⦋𝐴 / 𝑥⦌𝑓 ↾ ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦)) |
30 | | csbconstg 3800 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑓 = 𝑓) |
31 | 30, 18 | reseq12d 5696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝑓 ↾ ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑦)) = (𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))) |
32 | 29, 31 | syl5eq 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)) = (𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))) |
33 | 32 | fveq2d 6503 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))) |
34 | 28, 33 | syl5eq 2827 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))) |
35 | 27, 34 | eqeq12d 2794 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌(𝑓‘𝑦) = ⦋𝐴 / 𝑥⦌(𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))) |
36 | 26, 35 | bitrd 271 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))) |
37 | 36 | ralbidv 3148 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝑧 [𝐴 / 𝑥](𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))) |
38 | 25, 37 | bitrd 271 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))) ↔ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))) |
39 | 5, 24, 38 | 3anbi123d 1415 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝑓 Fn 𝑧 ∧ [𝐴 / 𝑥](𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ [𝐴 / 𝑥]∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ (𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))))) |
40 | 4, 39 | syl5bb 275 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ (𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))))) |
41 | 40 | exbidv 1880 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (∃𝑧[𝐴 / 𝑥](𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))))) |
42 | 3, 41 | syl5bb 275 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦)))) ↔ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦)))))) |
43 | 42 | abbidv 2844 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → {𝑓 ∣ [𝐴 / 𝑥]∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))}) |
44 | 2, 43 | syl5eq 2827 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))}) |
45 | 44 | unieqd 4722 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪
⦋𝐴 / 𝑥⦌{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = ∪ {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))}) |
46 | 1, 45 | syl5eq 2827 |
. 2
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪
{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} = ∪ {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))}) |
47 | | df-wrecs 7750 |
. . 3
⊢
wrecs(𝑅, 𝐷, 𝐹) = ∪ {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} |
48 | 47 | csbeq2i 4257 |
. 2
⊢
⦋𝐴 /
𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = ⦋𝐴 / 𝑥⦌∪
{𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ 𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(𝑅, 𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐷, 𝑦))))} |
49 | | df-wrecs 7750 |
. 2
⊢
wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹) = ∪ {𝑓 ∣ ∃𝑧(𝑓 Fn 𝑧 ∧ (𝑧 ⊆ ⦋𝐴 / 𝑥⦌𝐷 ∧ ∀𝑦 ∈ 𝑧 Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦) ⊆ 𝑧) ∧ ∀𝑦 ∈ 𝑧 (𝑓‘𝑦) = (⦋𝐴 / 𝑥⦌𝐹‘(𝑓 ↾ Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, 𝑦))))} |
50 | 46, 48, 49 | 3eqtr4g 2840 |
1
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) |