This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrdg2

Description: Alternate definition of the recursive function generator when I is a set. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg2 ( 𝐼 ∈ 𝑉 → rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rdgeq2 ⊢ ( 𝑖 = 𝐼 → rec ( 𝐹 , 𝑖 ) = rec ( 𝐹 , 𝐼 ) )
2 ifeq1 ⊢ ( 𝑖 = 𝐼 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
3 2 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
4 3 ralbidv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
5 4 anbi2d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
6 5 rexbidv ⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
7 6 abbidv ⊢ ( 𝑖 = 𝐼 → { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
8 7 unieqd ⊢ ( 𝑖 = 𝐼 → ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )
9 1 8 eqeq12d ⊢ ( 𝑖 = 𝐼 → ( rec ( 𝐹 , 𝑖 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } ↔ rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } ) )
10 df-rdg ⊢ rec ( 𝐹 , 𝑖 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
11 dfrecs3 ⊢ recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
12 vex ⊢ 𝑓 ∈ V
13 12 resex ⊢ ( 𝑓 ↾ 𝑦 ) ∈ V
14 eqeq1 ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ( 𝑔 = ∅ ↔ ( 𝑓 ↾ 𝑦 ) = ∅ ) )
15 relres ⊢ Rel ( 𝑓 ↾ 𝑦 )
16 reldm0 ⊢ ( Rel ( 𝑓 ↾ 𝑦 ) → ( ( 𝑓 ↾ 𝑦 ) = ∅ ↔ dom ( 𝑓 ↾ 𝑦 ) = ∅ ) )
17 15 16 ax-mp ⊢ ( ( 𝑓 ↾ 𝑦 ) = ∅ ↔ dom ( 𝑓 ↾ 𝑦 ) = ∅ )
18 14 17 bitrdi ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ( 𝑔 = ∅ ↔ dom ( 𝑓 ↾ 𝑦 ) = ∅ ) )
19 dmeq ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → dom 𝑔 = dom ( 𝑓 ↾ 𝑦 ) )
20 limeq ⊢ ( dom 𝑔 = dom ( 𝑓 ↾ 𝑦 ) → ( Lim dom 𝑔 ↔ Lim dom ( 𝑓 ↾ 𝑦 ) ) )
21 19 20 syl ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ( Lim dom 𝑔 ↔ Lim dom ( 𝑓 ↾ 𝑦 ) ) )
22 rneq ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ran 𝑔 = ran ( 𝑓 ↾ 𝑦 ) )
23 df-ima ⊢ ( 𝑓 “ 𝑦 ) = ran ( 𝑓 ↾ 𝑦 )
24 22 23 eqtr4di ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ran 𝑔 = ( 𝑓 “ 𝑦 ) )
25 24 unieqd ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ∪ ran 𝑔 = ∪ ( 𝑓 “ 𝑦 ) )
26 id ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → 𝑔 = ( 𝑓 ↾ 𝑦 ) )
27 19 unieqd ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ∪ dom 𝑔 = ∪ dom ( 𝑓 ↾ 𝑦 ) )
28 26 27 fveq12d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ( 𝑔 ‘ ∪ dom 𝑔 ) = ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) )
29 28 fveq2d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) )
30 21 25 29 ifbieq12d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) )
31 18 30 ifbieq2d ⊢ ( 𝑔 = ( 𝑓 ↾ 𝑦 ) → if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) )
32 eqid ⊢ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
33 vex ⊢ 𝑖 ∈ V
34 imaexg ⊢ ( 𝑓 ∈ V → ( 𝑓 “ 𝑦 ) ∈ V )
35 12 34 ax-mp ⊢ ( 𝑓 “ 𝑦 ) ∈ V
36 35 uniex ⊢ ∪ ( 𝑓 “ 𝑦 ) ∈ V
37 fvex ⊢ ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ∈ V
38 36 37 ifex ⊢ if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ∈ V
39 33 38 ifex ⊢ if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) ∈ V
40 31 32 39 fvmpt ⊢ ( ( 𝑓 ↾ 𝑦 ) ∈ V → ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) = if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) )
41 13 40 ax-mp ⊢ ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) = if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) )
42 dmres ⊢ dom ( 𝑓 ↾ 𝑦 ) = ( 𝑦 ∩ dom 𝑓 )
43 onelss ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
44 43 imp ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ 𝑥 )
45 44 3adant2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ 𝑥 )
46 fndm ⊢ ( 𝑓 Fn 𝑥 → dom 𝑓 = 𝑥 )
47 46 3ad2ant2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → dom 𝑓 = 𝑥 )
48 45 47 sseqtrrd ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ⊆ dom 𝑓 )
49 dfss2 ⊢ ( 𝑦 ⊆ dom 𝑓 ↔ ( 𝑦 ∩ dom 𝑓 ) = 𝑦 )
50 48 49 sylib ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∩ dom 𝑓 ) = 𝑦 )
51 42 50 eqtrid ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → dom ( 𝑓 ↾ 𝑦 ) = 𝑦 )
52 eqeq1 ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → ( dom ( 𝑓 ↾ 𝑦 ) = ∅ ↔ 𝑦 = ∅ ) )
53 limeq ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → ( Lim dom ( 𝑓 ↾ 𝑦 ) ↔ Lim 𝑦 ) )
54 unieq ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → ∪ dom ( 𝑓 ↾ 𝑦 ) = ∪ 𝑦 )
55 54 fveq2d ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) = ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) )
56 55 fveq2d ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) )
57 53 56 ifbieq2d ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) )
58 52 57 ifbieq2d ⊢ ( dom ( 𝑓 ↾ 𝑦 ) = 𝑦 → if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) )
59 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
60 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
61 59 60 syl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
62 61 3adant2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
63 ordzsl ⊢ ( Ord 𝑦 ↔ ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦 ) )
64 iftrue ⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = 𝑖 )
65 iftrue ⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = 𝑖 )
66 64 65 eqtr4d ⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
67 vex ⊢ 𝑧 ∈ V
68 67 sucid ⊢ 𝑧 ∈ suc 𝑧
69 fvres ⊢ ( 𝑧 ∈ suc 𝑧 → ( ( 𝑓 ↾ suc 𝑧 ) ‘ 𝑧 ) = ( 𝑓 ‘ 𝑧 ) )
70 68 69 ax-mp ⊢ ( ( 𝑓 ↾ suc 𝑧 ) ‘ 𝑧 ) = ( 𝑓 ‘ 𝑧 )
71 eloni ⊢ ( 𝑧 ∈ On → Ord 𝑧 )
72 ordunisuc ⊢ ( Ord 𝑧 → ∪ suc 𝑧 = 𝑧 )
73 71 72 syl ⊢ ( 𝑧 ∈ On → ∪ suc 𝑧 = 𝑧 )
74 73 fveq2d ⊢ ( 𝑧 ∈ On → ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) = ( ( 𝑓 ↾ suc 𝑧 ) ‘ 𝑧 ) )
75 73 fveq2d ⊢ ( 𝑧 ∈ On → ( 𝑓 ‘ ∪ suc 𝑧 ) = ( 𝑓 ‘ 𝑧 ) )
76 70 74 75 3eqtr4a ⊢ ( 𝑧 ∈ On → ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) = ( 𝑓 ‘ ∪ suc 𝑧 ) )
77 76 fveq2d ⊢ ( 𝑧 ∈ On → ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
78 nsuceq0 ⊢ suc 𝑧 ≠ ∅
79 78 neii ⊢ ¬ suc 𝑧 = ∅
80 79 iffalsei ⊢ if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) )
81 nlimsucg ⊢ ( 𝑧 ∈ V → ¬ Lim suc 𝑧 )
82 iffalse ⊢ ( ¬ Lim suc 𝑧 → if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) )
83 67 81 82 mp2b ⊢ if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) )
84 80 83 eqtri ⊢ if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) )
85 79 iffalsei ⊢ if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
86 iffalse ⊢ ( ¬ Lim suc 𝑧 → if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
87 67 81 86 mp2b ⊢ if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) )
88 85 87 eqtri ⊢ if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) )
89 77 84 88 3eqtr4g ⊢ ( 𝑧 ∈ On → if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) ) = if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) )
90 eqeq1 ⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 = ∅ ↔ suc 𝑧 = ∅ ) )
91 limeq ⊢ ( 𝑦 = suc 𝑧 → ( Lim 𝑦 ↔ Lim suc 𝑧 ) )
92 reseq2 ⊢ ( 𝑦 = suc 𝑧 → ( 𝑓 ↾ 𝑦 ) = ( 𝑓 ↾ suc 𝑧 ) )
93 unieq ⊢ ( 𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧 )
94 92 93 fveq12d ⊢ ( 𝑦 = suc 𝑧 → ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) = ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) )
95 94 fveq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) = ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) )
96 91 95 ifbieq2d ⊢ ( 𝑦 = suc 𝑧 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) )
97 90 96 ifbieq2d ⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) ) )
98 93 fveq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝑓 ‘ ∪ 𝑦 ) = ( 𝑓 ‘ ∪ suc 𝑧 ) )
99 98 fveq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
100 91 99 ifbieq2d ⊢ ( 𝑦 = suc 𝑧 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) )
101 90 100 ifbieq2d ⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) )
102 97 101 eqeq12d ⊢ ( 𝑦 = suc 𝑧 → ( if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ suc 𝑧 ) ‘ ∪ suc 𝑧 ) ) ) ) = if ( suc 𝑧 = ∅ , 𝑖 , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) ) )
103 89 102 syl5ibrcom ⊢ ( 𝑧 ∈ On → ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
104 103 rexlimiv ⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
105 iftrue ⊢ ( Lim 𝑦 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) = ∪ ( 𝑓 “ 𝑦 ) )
106 df-lim ⊢ ( Lim 𝑦 ↔ ( Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦 ) )
107 106 simp2bi ⊢ ( Lim 𝑦 → 𝑦 ≠ ∅ )
108 107 neneqd ⊢ ( Lim 𝑦 → ¬ 𝑦 = ∅ )
109 108 iffalsed ⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) )
110 iftrue ⊢ ( Lim 𝑦 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = ∪ ( 𝑓 “ 𝑦 ) )
111 105 109 110 3eqtr4d ⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
112 108 iffalsed ⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
113 111 112 eqtr4d ⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
114 66 104 113 3jaoi ⊢ ( ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ Lim 𝑦 ) → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
115 63 114 sylbi ⊢ ( Ord 𝑦 → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
116 62 115 syl ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ 𝑦 ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
117 58 116 sylan9eqr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) ∧ dom ( 𝑓 ↾ 𝑦 ) = 𝑦 ) → if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
118 51 117 mpdan ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → if ( dom ( 𝑓 ↾ 𝑦 ) = ∅ , 𝑖 , if ( Lim dom ( 𝑓 ↾ 𝑦 ) , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( ( 𝑓 ↾ 𝑦 ) ‘ ∪ dom ( 𝑓 ↾ 𝑦 ) ) ) ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
119 41 118 eqtrid ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
120 119 eqeq2d ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
121 120 3expa ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
122 121 ralbidva ⊢ ( ( 𝑥 ∈ On ∧ 𝑓 Fn 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
123 122 pm5.32da ⊢ ( 𝑥 ∈ On → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
124 123 rexbiia ⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
125 124 abbii ⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }
126 125 unieqi ⊢ ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝑖 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }
127 10 11 126 3eqtri ⊢ rec ( 𝐹 , 𝑖 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝑖 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }
128 9 127 vtoclg ⊢ ( 𝐼 ∈ 𝑉 → rec ( 𝐹 , 𝐼 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , 𝐼 , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) } )