Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfrdg2 Structured version   Visualization version   GIF version

Theorem dfrdg2 35777
Description: Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
dfrdg2 (𝐼𝑉 → rec(𝐹, 𝐼) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))})
Distinct variable groups:   𝑓,𝐹,𝑥,𝑦   𝑓,𝐼,𝑥,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑓)

Proof of Theorem dfrdg2
Dummy variables 𝑔 𝑖 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rdgeq2 8451 . . 3 (𝑖 = 𝐼 → rec(𝐹, 𝑖) = rec(𝐹, 𝐼))
2 ifeq1 4535 . . . . . . . . 9 (𝑖 = 𝐼 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
32eqeq2d 2746 . . . . . . . 8 (𝑖 = 𝐼 → ((𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
43ralbidv 3176 . . . . . . 7 (𝑖 = 𝐼 → (∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
54anbi2d 630 . . . . . 6 (𝑖 = 𝐼 → ((𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
65rexbidv 3177 . . . . 5 (𝑖 = 𝐼 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
76abbidv 2806 . . . 4 (𝑖 = 𝐼 → {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))})
87unieqd 4925 . . 3 (𝑖 = 𝐼 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))})
91, 8eqeq12d 2751 . 2 (𝑖 = 𝐼 → (rec(𝐹, 𝑖) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))} ↔ rec(𝐹, 𝐼) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}))
10 df-rdg 8449 . . 3 rec(𝐹, 𝑖) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))))))
11 dfrecs3 8411 . . 3 recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)))}
12 vex 3482 . . . . . . . . . . . . 13 𝑓 ∈ V
1312resex 6049 . . . . . . . . . . . 12 (𝑓𝑦) ∈ V
14 eqeq1 2739 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓𝑦) → (𝑔 = ∅ ↔ (𝑓𝑦) = ∅))
15 relres 6026 . . . . . . . . . . . . . . . 16 Rel (𝑓𝑦)
16 reldm0 5941 . . . . . . . . . . . . . . . 16 (Rel (𝑓𝑦) → ((𝑓𝑦) = ∅ ↔ dom (𝑓𝑦) = ∅))
1715, 16ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑓𝑦) = ∅ ↔ dom (𝑓𝑦) = ∅)
1814, 17bitrdi 287 . . . . . . . . . . . . . 14 (𝑔 = (𝑓𝑦) → (𝑔 = ∅ ↔ dom (𝑓𝑦) = ∅))
19 dmeq 5917 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓𝑦) → dom 𝑔 = dom (𝑓𝑦))
20 limeq 6398 . . . . . . . . . . . . . . . 16 (dom 𝑔 = dom (𝑓𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓𝑦)))
2119, 20syl 17 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓𝑦) → (Lim dom 𝑔 ↔ Lim dom (𝑓𝑦)))
22 rneq 5950 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑓𝑦) → ran 𝑔 = ran (𝑓𝑦))
23 df-ima 5702 . . . . . . . . . . . . . . . . 17 (𝑓𝑦) = ran (𝑓𝑦)
2422, 23eqtr4di 2793 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓𝑦) → ran 𝑔 = (𝑓𝑦))
2524unieqd 4925 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓𝑦) → ran 𝑔 = (𝑓𝑦))
26 id 22 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑓𝑦) → 𝑔 = (𝑓𝑦))
2719unieqd 4925 . . . . . . . . . . . . . . . . 17 (𝑔 = (𝑓𝑦) → dom 𝑔 = dom (𝑓𝑦))
2826, 27fveq12d 6914 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓𝑦) → (𝑔 dom 𝑔) = ((𝑓𝑦)‘ dom (𝑓𝑦)))
2928fveq2d 6911 . . . . . . . . . . . . . . 15 (𝑔 = (𝑓𝑦) → (𝐹‘(𝑔 dom 𝑔)) = (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))
3021, 25, 29ifbieq12d 4559 . . . . . . . . . . . . . 14 (𝑔 = (𝑓𝑦) → if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))) = if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦)))))
3118, 30ifbieq2d 4557 . . . . . . . . . . . . 13 (𝑔 = (𝑓𝑦) → if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))) = if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))))
32 eqid 2735 . . . . . . . . . . . . 13 (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))))) = (𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))
33 vex 3482 . . . . . . . . . . . . . 14 𝑖 ∈ V
34 imaexg 7936 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ V → (𝑓𝑦) ∈ V)
3512, 34ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑓𝑦) ∈ V
3635uniex 7760 . . . . . . . . . . . . . . 15 (𝑓𝑦) ∈ V
37 fvex 6920 . . . . . . . . . . . . . . 15 (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))) ∈ V
3836, 37ifex 4581 . . . . . . . . . . . . . 14 if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦)))) ∈ V
3933, 38ifex 4581 . . . . . . . . . . . . 13 if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))) ∈ V
4031, 32, 39fvmpt 7016 . . . . . . . . . . . 12 ((𝑓𝑦) ∈ V → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) = if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))))
4113, 40ax-mp 5 . . . . . . . . . . 11 ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) = if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦)))))
42 dmres 6032 . . . . . . . . . . . . 13 dom (𝑓𝑦) = (𝑦 ∩ dom 𝑓)
43 onelss 6428 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ On → (𝑦𝑥𝑦𝑥))
4443imp 406 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦𝑥)
45443adant2 1130 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → 𝑦𝑥)
46 fndm 6672 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
47463ad2ant2 1133 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → dom 𝑓 = 𝑥)
4845, 47sseqtrrd 4037 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → 𝑦 ⊆ dom 𝑓)
49 dfss2 3981 . . . . . . . . . . . . . 14 (𝑦 ⊆ dom 𝑓 ↔ (𝑦 ∩ dom 𝑓) = 𝑦)
5048, 49sylib 218 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → (𝑦 ∩ dom 𝑓) = 𝑦)
5142, 50eqtrid 2787 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → dom (𝑓𝑦) = 𝑦)
52 eqeq1 2739 . . . . . . . . . . . . . 14 (dom (𝑓𝑦) = 𝑦 → (dom (𝑓𝑦) = ∅ ↔ 𝑦 = ∅))
53 limeq 6398 . . . . . . . . . . . . . . 15 (dom (𝑓𝑦) = 𝑦 → (Lim dom (𝑓𝑦) ↔ Lim 𝑦))
54 unieq 4923 . . . . . . . . . . . . . . . . 17 (dom (𝑓𝑦) = 𝑦 dom (𝑓𝑦) = 𝑦)
5554fveq2d 6911 . . . . . . . . . . . . . . . 16 (dom (𝑓𝑦) = 𝑦 → ((𝑓𝑦)‘ dom (𝑓𝑦)) = ((𝑓𝑦)‘ 𝑦))
5655fveq2d 6911 . . . . . . . . . . . . . . 15 (dom (𝑓𝑦) = 𝑦 → (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))) = (𝐹‘((𝑓𝑦)‘ 𝑦)))
5753, 56ifbieq2d 4557 . . . . . . . . . . . . . 14 (dom (𝑓𝑦) = 𝑦 → if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦))))
5852, 57ifbieq2d 4557 . . . . . . . . . . . . 13 (dom (𝑓𝑦) = 𝑦 → if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))))
59 onelon 6411 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
60 eloni 6396 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → Ord 𝑦)
6159, 60syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑦𝑥) → Ord 𝑦)
62613adant2 1130 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → Ord 𝑦)
63 ordzsl 7866 . . . . . . . . . . . . . . 15 (Ord 𝑦 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦))
64 iftrue 4537 . . . . . . . . . . . . . . . . 17 (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = 𝑖)
65 iftrue 4537 . . . . . . . . . . . . . . . . 17 (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = 𝑖)
6664, 65eqtr4d 2778 . . . . . . . . . . . . . . . 16 (𝑦 = ∅ → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
67 vex 3482 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧 ∈ V
6867sucid 6468 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ suc 𝑧
69 fvres 6926 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ suc 𝑧 → ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓𝑧))
7068, 69ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ↾ suc 𝑧)‘𝑧) = (𝑓𝑧)
71 eloni 6396 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ On → Ord 𝑧)
72 ordunisuc 7852 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑧 suc 𝑧 = 𝑧)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ On → suc 𝑧 = 𝑧)
7473fveq2d 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘ suc 𝑧) = ((𝑓 ↾ suc 𝑧)‘𝑧))
7573fveq2d 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ On → (𝑓 suc 𝑧) = (𝑓𝑧))
7670, 74, 753eqtr4a 2801 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ On → ((𝑓 ↾ suc 𝑧)‘ suc 𝑧) = (𝑓 suc 𝑧))
7776fveq2d 6911 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ On → (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)) = (𝐹‘(𝑓 suc 𝑧)))
78 nsuceq0 6469 . . . . . . . . . . . . . . . . . . . . . 22 suc 𝑧 ≠ ∅
7978neii 2940 . . . . . . . . . . . . . . . . . . . . 21 ¬ suc 𝑧 = ∅
8079iffalsei 4541 . . . . . . . . . . . . . . . . . . . 20 if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))
81 nlimsucg 7863 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ V → ¬ Lim suc 𝑧)
82 iffalse 4540 . . . . . . . . . . . . . . . . . . . . 21 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))
8367, 81, 82mp2b 10 . . . . . . . . . . . . . . . . . . . 20 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧))
8480, 83eqtri 2763 . . . . . . . . . . . . . . . . . . 19 if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))) = (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧))
8579iffalsei 4541 . . . . . . . . . . . . . . . . . . . 20 if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))
86 iffalse 4540 . . . . . . . . . . . . . . . . . . . . 21 (¬ Lim suc 𝑧 → if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧)))
8767, 81, 86mp2b 10 . . . . . . . . . . . . . . . . . . . 20 if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))) = (𝐹‘(𝑓 suc 𝑧))
8885, 87eqtri 2763 . . . . . . . . . . . . . . . . . . 19 if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))) = (𝐹‘(𝑓 suc 𝑧))
8977, 84, 883eqtr4g 2800 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ On → if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
90 eqeq1 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
91 limeq 6398 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
92 reseq2 5995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = suc 𝑧 → (𝑓𝑦) = (𝑓 ↾ suc 𝑧))
93 unieq 4923 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = suc 𝑧 𝑦 = suc 𝑧)
9492, 93fveq12d 6914 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = suc 𝑧 → ((𝑓𝑦)‘ 𝑦) = ((𝑓 ↾ suc 𝑧)‘ suc 𝑧))
9594fveq2d 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = suc 𝑧 → (𝐹‘((𝑓𝑦)‘ 𝑦)) = (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))
9691, 95ifbieq2d 4557 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧))))
9790, 96ifbieq2d 4557 . . . . . . . . . . . . . . . . . . 19 (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))))
9893fveq2d 6911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = suc 𝑧 → (𝑓 𝑦) = (𝑓 suc 𝑧))
9998fveq2d 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = suc 𝑧 → (𝐹‘(𝑓 𝑦)) = (𝐹‘(𝑓 suc 𝑧)))
10091, 99ifbieq2d 4557 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = suc 𝑧 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))
10190, 100ifbieq2d 4557 . . . . . . . . . . . . . . . . . . 19 (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧)))))
10297, 101eqeq12d 2751 . . . . . . . . . . . . . . . . . 18 (𝑦 = suc 𝑧 → (if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) ↔ if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘((𝑓 ↾ suc 𝑧)‘ suc 𝑧)))) = if(suc 𝑧 = ∅, 𝑖, if(Lim suc 𝑧, (𝑓𝑦), (𝐹‘(𝑓 suc 𝑧))))))
10389, 102syl5ibrcom 247 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ On → (𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
104103rexlimiv 3146 . . . . . . . . . . . . . . . 16 (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
105 iftrue 4537 . . . . . . . . . . . . . . . . . 18 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦))) = (𝑓𝑦))
106 df-lim 6391 . . . . . . . . . . . . . . . . . . . . 21 (Lim 𝑦 ↔ (Ord 𝑦𝑦 ≠ ∅ ∧ 𝑦 = 𝑦))
107106simp2bi 1145 . . . . . . . . . . . . . . . . . . . 20 (Lim 𝑦𝑦 ≠ ∅)
108107neneqd 2943 . . . . . . . . . . . . . . . . . . 19 (Lim 𝑦 → ¬ 𝑦 = ∅)
109108iffalsed 4542 . . . . . . . . . . . . . . . . . 18 (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦))))
110 iftrue 4537 . . . . . . . . . . . . . . . . . 18 (Lim 𝑦 → if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))) = (𝑓𝑦))
111105, 109, 1103eqtr4d 2785 . . . . . . . . . . . . . . . . 17 (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
112108iffalsed 4542 . . . . . . . . . . . . . . . . 17 (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))) = if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))
113111, 112eqtr4d 2778 . . . . . . . . . . . . . . . 16 (Lim 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11466, 104, 1133jaoi 1427 . . . . . . . . . . . . . . 15 ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11563, 114sylbi 217 . . . . . . . . . . . . . 14 (Ord 𝑦 → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11662, 115syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ 𝑦)))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11758, 116sylan9eqr 2797 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) ∧ dom (𝑓𝑦) = 𝑦) → if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11851, 117mpdan 687 . . . . . . . . . . 11 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → if(dom (𝑓𝑦) = ∅, 𝑖, if(Lim dom (𝑓𝑦), (𝑓𝑦), (𝐹‘((𝑓𝑦)‘ dom (𝑓𝑦))))) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
11941, 118eqtrid 2787 . . . . . . . . . 10 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))
120119eqeq2d 2746 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥𝑦𝑥) → ((𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) ↔ (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
1211203expa 1117 . . . . . . . 8 (((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) ∧ 𝑦𝑥) → ((𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) ↔ (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
122121ralbidva 3174 . . . . . . 7 ((𝑥 ∈ On ∧ 𝑓 Fn 𝑥) → (∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
123122pm5.32da 579 . . . . . 6 (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦))) ↔ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))))
124123rexbiia 3090 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦))))))
125124abbii 2807 . . . 4 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
126125unieqi 4924 . . 3 {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝑖, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))‘(𝑓𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
12710, 11, 1263eqtri 2767 . 2 rec(𝐹, 𝑖) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝑖, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))}
1289, 127vtoclg 3554 1 (𝐼𝑉 → rec(𝐹, 𝐼) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, (𝑓𝑦), (𝐹‘(𝑓 𝑦)))))})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3o 1085  w3a 1086   = wceq 1537  wcel 2106  {cab 2712  wne 2938  wral 3059  wrex 3068  Vcvv 3478  cin 3962  wss 3963  c0 4339  ifcif 4531   cuni 4912  cmpt 5231  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  Rel wrel 5694  Ord word 6385  Oncon0 6386  Lim wlim 6387  suc csuc 6388   Fn wfn 6558  cfv 6563  recscrecs 8409  reccrdg 8448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fo 6569  df-fv 6571  df-ov 7434  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449
This theorem is referenced by:  dfrdg3  35778
  Copyright terms: Public domain W3C validator