Step | Hyp | Ref
| Expression |
1 | | rdgeq2 8148 |
. . 3
⊢ (𝑖 = 𝐼 → rec(𝐹, 𝑖) = rec(𝐹, 𝐼)) |
2 | | ifeq1 4443 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
3 | 2 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → ((𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
4 | 3 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
5 | 4 | anbi2d 632 |
. . . . . 6
⊢ (𝑖 = 𝐼 → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
6 | 5 | rexbidv 3216 |
. . . . 5
⊢ (𝑖 = 𝐼 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
7 | 6 | abbidv 2807 |
. . . 4
⊢ (𝑖 = 𝐼 → {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}) |
8 | 7 | unieqd 4833 |
. . 3
⊢ (𝑖 = 𝐼 → ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}) |
9 | 1, 8 | eqeq12d 2753 |
. 2
⊢ (𝑖 = 𝐼 → (rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} ↔ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})) |
10 | | df-rdg 8146 |
. . 3
⊢ rec(𝐹, 𝑖) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) |
11 | | dfrecs3 8109 |
. . 3
⊢
recs((𝑔 ∈ V
↦ if(𝑔 = ∅,
𝑖, if(Lim dom 𝑔, ∪
ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))) = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} |
12 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑓 ∈ V |
13 | 12 | resex 5899 |
. . . . . . . . . . . 12
⊢ (𝑓 ↾ 𝑦) ∈ V |
14 | | eqeq1 2741 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ (𝑓 ↾ 𝑦) = ∅)) |
15 | | relres 5880 |
. . . . . . . . . . . . . . . 16
⊢ Rel
(𝑓 ↾ 𝑦) |
16 | | reldm0 5797 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
(𝑓 ↾ 𝑦) → ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅)) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ↾ 𝑦) = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅) |
18 | 14, 17 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔 = ∅ ↔ dom (𝑓 ↾ 𝑦) = ∅)) |
19 | | dmeq 5772 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ↾ 𝑦) → dom 𝑔 = dom (𝑓 ↾ 𝑦)) |
20 | | limeq 6225 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑔 = dom (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ 𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓 ↾ 𝑦))) |
22 | | rneq 5805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = ran (𝑓 ↾ 𝑦)) |
23 | | df-ima 5564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 “ 𝑦) = ran (𝑓 ↾ 𝑦) |
24 | 22, 23 | eqtr4di 2796 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ↾ 𝑦) → ran 𝑔 = (𝑓 “ 𝑦)) |
25 | 24 | unieqd 4833 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ ran
𝑔 = ∪ (𝑓
“ 𝑦)) |
26 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (𝑓 ↾ 𝑦) → 𝑔 = (𝑓 ↾ 𝑦)) |
27 | 19 | unieqd 4833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (𝑓 ↾ 𝑦) → ∪ dom
𝑔 = ∪ dom (𝑓 ↾ 𝑦)) |
28 | 26, 27 | fveq12d 6724 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝑔‘∪ dom 𝑔) = ((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))) |
29 | 28 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ↾ 𝑦) → (𝐹‘(𝑔‘∪ dom 𝑔)) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)))) |
30 | 21, 25, 29 | ifbieq12d 4467 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))) = if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) |
31 | 18, 30 | ifbieq2d 4465 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ↾ 𝑦) → if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)))))) |
32 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔))))) |
33 | | vex 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑖 ∈ V |
34 | | imaexg 7693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ V → (𝑓 “ 𝑦) ∈ V) |
35 | 12, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 “ 𝑦) ∈ V |
36 | 35 | uniex 7529 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝑓
“ 𝑦) ∈
V |
37 | | fvex 6730 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))) ∈ V |
38 | 36, 37 | ifex 4489 |
. . . . . . . . . . . . . 14
⊢ if(Lim
dom (𝑓 ↾ 𝑦), ∪
(𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)))) ∈ V |
39 | 33, 38 | ifex 4489 |
. . . . . . . . . . . . 13
⊢ if(dom
(𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) ∈ V |
40 | 31, 32, 39 | fvmpt 6818 |
. . . . . . . . . . . 12
⊢ ((𝑓 ↾ 𝑦) ∈ V → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)))))) |
41 | 13, 40 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) |
42 | | dmres 5873 |
. . . . . . . . . . . . 13
⊢ dom
(𝑓 ↾ 𝑦) = (𝑦 ∩ dom 𝑓) |
43 | | onelss 6255 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥)) |
44 | 43 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥) |
45 | 44 | 3adant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ 𝑥) |
46 | | fndm 6481 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥) |
47 | 46 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom 𝑓 = 𝑥) |
48 | 45, 47 | sseqtrrd 3942 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ⊆ dom 𝑓) |
49 | | df-ss 3883 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ dom 𝑓 ↔ (𝑦 ∩ dom 𝑓) = 𝑦) |
50 | 48, 49 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ dom 𝑓) = 𝑦) |
51 | 42, 50 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → dom (𝑓 ↾ 𝑦) = 𝑦) |
52 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → (dom (𝑓 ↾ 𝑦) = ∅ ↔ 𝑦 = ∅)) |
53 | | limeq 6225 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → (Lim dom (𝑓 ↾ 𝑦) ↔ Lim 𝑦)) |
54 | | unieq 4830 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → ∪ dom
(𝑓 ↾ 𝑦) = ∪
𝑦) |
55 | 54 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → ((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)) = ((𝑓 ↾ 𝑦)‘∪ 𝑦)) |
56 | 55 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))) = (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) |
57 | 53, 56 | ifbieq2d 4465 |
. . . . . . . . . . . . . 14
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) |
58 | 52, 57 | ifbieq2d 4465 |
. . . . . . . . . . . . 13
⊢ (dom
(𝑓 ↾ 𝑦) = 𝑦 → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))))) |
59 | | onelon 6238 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
60 | | eloni 6223 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → Ord 𝑦) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
62 | 61 | 3adant2 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
63 | | ordzsl 7624 |
. . . . . . . . . . . . . . 15
⊢ (Ord
𝑦 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦)) |
64 | | iftrue 4445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = 𝑖) |
65 | | iftrue 4445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = 𝑖) |
66 | 64, 65 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
67 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑧 ∈ V |
68 | 67 | sucid 6292 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑧 ∈ suc 𝑧 |
69 | | fvres 6736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ suc 𝑧 → ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧)) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓‘𝑧) |
71 | | eloni 6223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ On → Ord 𝑧) |
72 | | ordunisuc 7611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑧 → ∪ suc 𝑧 = 𝑧) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ On → ∪ suc 𝑧 = 𝑧) |
74 | 73 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧) = ((𝑓 ↾ suc 𝑧)‘𝑧)) |
75 | 73 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ On → (𝑓‘∪ suc 𝑧) = (𝑓‘𝑧)) |
76 | 70, 74, 75 | 3eqtr4a 2804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧) = (𝑓‘∪ suc 𝑧)) |
77 | 76 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ On → (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
78 | | nsuceq0 6293 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ suc 𝑧 ≠ ∅ |
79 | 78 | neii 2942 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
suc 𝑧 =
∅ |
80 | 79 | iffalsei 4449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(suc
𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))) |
81 | | nlimsucg 7621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ V → ¬ Lim suc
𝑧) |
82 | | iffalse 4448 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
Lim suc 𝑧 → if(Lim suc
𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))) |
83 | 67, 81, 82 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(Lim
suc 𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)) |
84 | 80, 83 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ if(suc
𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)) |
85 | 79 | iffalsei 4449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(suc
𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) |
86 | | iffalse 4448 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
Lim suc 𝑧 → if(Lim suc
𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
87 | 67, 81, 86 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(Lim
suc 𝑧, ∪ (𝑓
“ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
88 | 85, 87 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ if(suc
𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧)) |
89 | 77, 84, 88 | 3eqtr4g 2803 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ On → if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))) |
90 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅)) |
91 | | limeq 6225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧)) |
92 | | reseq2 5846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = suc 𝑧 → (𝑓 ↾ 𝑦) = (𝑓 ↾ suc 𝑧)) |
93 | | unieq 4830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪
suc 𝑧) |
94 | 92, 93 | fveq12d 6724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = suc 𝑧 → ((𝑓 ↾ 𝑦)‘∪ 𝑦) = ((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)) |
95 | 94 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = suc 𝑧 → (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)) = (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))) |
96 | 91, 95 | ifbieq2d 4465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)))) |
97 | 90, 96 | ifbieq2d 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧))))) |
98 | 93 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧)) |
99 | 98 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧))) |
100 | 91, 99 | ifbieq2d 4465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) |
101 | 90, 100 | ifbieq2d 4465 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))) |
102 | 97, 101 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = suc 𝑧 → (if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘∪ suc
𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))) |
103 | 89, 102 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ On → (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
104 | 103 | rexlimiv 3199 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑧 ∈ On
𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
105 | | iftrue 4445 |
. . . . . . . . . . . . . . . . . 18
⊢ (Lim
𝑦 → if(Lim 𝑦, ∪
(𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦))) = ∪ (𝑓
“ 𝑦)) |
106 | | df-lim 6218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Lim
𝑦 ↔ (Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦)) |
107 | 106 | simp2bi 1148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝑦 → 𝑦 ≠ ∅) |
108 | 107 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝑦 → ¬ 𝑦 = ∅) |
109 | 108 | iffalsed 4450 |
. . . . . . . . . . . . . . . . . 18
⊢ (Lim
𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) |
110 | | iftrue 4445 |
. . . . . . . . . . . . . . . . . 18
⊢ (Lim
𝑦 → if(Lim 𝑦, ∪
(𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓
“ 𝑦)) |
111 | 105, 109,
110 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) |
112 | 108 | iffalsed 4450 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) |
113 | 111, 112 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
114 | 66, 104, 113 | 3jaoi 1429 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
115 | 63, 114 | sylbi 220 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
116 | 62, 115 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
117 | 58, 116 | sylan9eqr 2800 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) ∧ dom (𝑓 ↾ 𝑦) = 𝑦) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
118 | 51, 117 | mpdan 687 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → if(dom (𝑓 ↾ 𝑦) = ∅, 𝑖, if(Lim dom (𝑓 ↾ 𝑦), ∪ (𝑓 “ 𝑦), (𝐹‘((𝑓 ↾ 𝑦)‘∪ dom
(𝑓 ↾ 𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
119 | 41, 118 | syl5eq 2790 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) |
120 | 119 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
121 | 120 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
122 | 121 | ralbidva 3117 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
123 | 122 | pm5.32da 582 |
. . . . . 6
⊢ (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) |
124 | 123 | rexbiia 3169 |
. . . . 5
⊢
(∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) |
125 | 124 | abbii 2808 |
. . . 4
⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
126 | 125 | unieqi 4832 |
. . 3
⊢ ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(𝑓 ↾ 𝑦)))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
127 | 10, 11, 126 | 3eqtri 2769 |
. 2
⊢ rec(𝐹, 𝑖) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} |
128 | 9, 127 | vtoclg 3481 |
1
⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}) |