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 df-ss ⊒ ( 𝑦 βŠ† 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 𝑦 , βˆͺ ( 𝑓 β€œ 𝑦 ) , ( 𝐹 β€˜ ( 𝑓 β€˜ βˆͺ 𝑦 ) ) ) ) ) } )