Step | Hyp | Ref
| Expression |
1 | | suceq 4139 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → suc 𝑛 = suc 𝑚) |
2 | 1 | eqeq2d 2051 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (dom 𝑓 = suc 𝑛 ↔ dom 𝑓 = suc 𝑚)) |
3 | | fveq2 5178 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
4 | 3 | fveq2d 5182 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑓‘𝑛)) = (𝐹‘(𝑓‘𝑚))) |
5 | 4 | eleq2d 2107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐹‘(𝑓‘𝑛)) ↔ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))) |
6 | 2, 5 | anbi12d 442 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))))) |
7 | 6 | cbvrexv 2534 |
. . . . . . 7
⊢
(∃𝑛 ∈
ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚)))) |
8 | 7 | orbi1i 680 |
. . . . . 6
⊢
((∃𝑛 ∈
ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))) |
9 | 8 | abbii 2153 |
. . . . 5
⊢ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} |
10 | | eleq1 2100 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (𝐹‘(𝑓‘𝑚)) ↔ 𝑦 ∈ (𝐹‘(𝑓‘𝑚)))) |
11 | 10 | anbi2d 437 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ↔ (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))))) |
12 | 11 | rexbidv 2327 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))))) |
13 | | eleq1 2100 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
14 | 13 | anbi2d 437 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))) |
15 | 12, 14 | orbi12d 707 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴)))) |
16 | 15 | cbvabv 2161 |
. . . . 5
⊢ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))} |
17 | 9, 16 | eqtri 2060 |
. . . 4
⊢ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))} = {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))} |
18 | 17 | mpteq2i 3844 |
. . 3
⊢ (𝑓 ∈ V ↦ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))}) = (𝑓 ∈ V ↦ {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))}) |
19 | | dmeq 4535 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔) |
20 | 19 | eqeq1d 2048 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (dom 𝑓 = suc 𝑚 ↔ dom 𝑔 = suc 𝑚)) |
21 | | fveq1 5177 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑓‘𝑚) = (𝑔‘𝑚)) |
22 | 21 | fveq2d 5182 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝐹‘(𝑓‘𝑚)) = (𝐹‘(𝑔‘𝑚))) |
23 | 22 | eleq2d 2107 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝑦 ∈ (𝐹‘(𝑓‘𝑚)) ↔ 𝑦 ∈ (𝐹‘(𝑔‘𝑚)))) |
24 | 20, 23 | anbi12d 442 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → ((dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ↔ (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))))) |
25 | 24 | rexbidv 2327 |
. . . . . 6
⊢ (𝑓 = 𝑔 → (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ↔ ∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))))) |
26 | 19 | eqeq1d 2048 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (dom 𝑓 = ∅ ↔ dom 𝑔 = ∅)) |
27 | 26 | anbi1d 438 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴) ↔ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))) |
28 | 25, 27 | orbi12d 707 |
. . . . 5
⊢ (𝑓 = 𝑔 → ((∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴)))) |
29 | 28 | abbidv 2155 |
. . . 4
⊢ (𝑓 = 𝑔 → {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))} = {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))}) |
30 | 29 | cbvmptv 3852 |
. . 3
⊢ (𝑓 ∈ V ↦ {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑓 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑓‘𝑚))) ∨ (dom 𝑓 = ∅ ∧ 𝑦 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))}) |
31 | 18, 30 | eqtri 2060 |
. 2
⊢ (𝑓 ∈ V ↦ {𝑥 ∣ (∃𝑛 ∈ ω (dom 𝑓 = suc 𝑛 ∧ 𝑥 ∈ (𝐹‘(𝑓‘𝑛))) ∨ (dom 𝑓 = ∅ ∧ 𝑥 ∈ 𝐴))}) = (𝑔 ∈ V ↦ {𝑦 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑦 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑦 ∈ 𝐴))}) |
32 | 31 | frecsuclem3 5990 |
1
⊢
((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) |