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

Metamath Proof Explorer

Theorem dfrecs2

Description: A quantifier-free definition of recs . (Contributed by Scott Fenton, 17-Jul-2020)

Ref Expression
Assertion dfrecs2 recs ( 𝐹 ) = ∪ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) )

Proof

Step Hyp Ref Expression
1 dfrecs3 ⊢ recs ( 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 elin ⊢ ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ↔ ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ◡ Domain “ On ) ) )
3 vex ⊢ 𝑓 ∈ V
4 3 elfuns ⊢ ( 𝑓 ∈ Funs ↔ Fun 𝑓 )
5 vex ⊢ 𝑥 ∈ V
6 5 3 brcnv ⊢ ( 𝑥 ◡ Domain 𝑓 ↔ 𝑓 Domain 𝑥 )
7 3 5 brdomain ⊢ ( 𝑓 Domain 𝑥 ↔ 𝑥 = dom 𝑓 )
8 6 7 bitri ⊢ ( 𝑥 ◡ Domain 𝑓 ↔ 𝑥 = dom 𝑓 )
9 8 rexbii ⊢ ( ∃ 𝑥 ∈ On 𝑥 ◡ Domain 𝑓 ↔ ∃ 𝑥 ∈ On 𝑥 = dom 𝑓 )
10 3 elima ⊢ ( 𝑓 ∈ ( ◡ Domain “ On ) ↔ ∃ 𝑥 ∈ On 𝑥 ◡ Domain 𝑓 )
11 risset ⊢ ( dom 𝑓 ∈ On ↔ ∃ 𝑥 ∈ On 𝑥 = dom 𝑓 )
12 9 10 11 3bitr4i ⊢ ( 𝑓 ∈ ( ◡ Domain “ On ) ↔ dom 𝑓 ∈ On )
13 4 12 anbi12i ⊢ ( ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) )
14 2 13 bitri ⊢ ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) )
15 3 eldm ⊢ ( 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ↔ ∃ 𝑦 𝑓 ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) 𝑦 )
16 brdif ⊢ ( 𝑓 ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) 𝑦 ↔ ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ∧ ¬ 𝑓 Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) 𝑦 ) )
17 vex ⊢ 𝑦 ∈ V
18 3 17 brco ⊢ ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ↔ ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) )
19 7 anbi1i ⊢ ( ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) )
20 19 exbii ⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) )
21 3 dmex ⊢ dom 𝑓 ∈ V
22 breq1 ⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ◡ E 𝑦 ↔ dom 𝑓 ◡ E 𝑦 ) )
23 21 22 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ◡ E 𝑦 ) ↔ dom 𝑓 ◡ E 𝑦 )
24 20 23 bitri ⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ◡ E 𝑦 ) ↔ dom 𝑓 ◡ E 𝑦 )
25 21 17 brcnv ⊢ ( dom 𝑓 ◡ E 𝑦 ↔ 𝑦 E dom 𝑓 )
26 21 epeli ⊢ ( 𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓 )
27 25 26 bitri ⊢ ( dom 𝑓 ◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓 )
28 18 24 27 3bitri ⊢ ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ↔ 𝑦 ∈ dom 𝑓 )
29 df-br ⊢ ( 𝑓 Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) 𝑦 ↔ ⟨ 𝑓 , 𝑦 ⟩ ∈ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) )
30 opex ⊢ ⟨ 𝑓 , 𝑦 ⟩ ∈ V
31 30 elfix ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ↔ ⟨ 𝑓 , 𝑦 ⟩ ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ⟨ 𝑓 , 𝑦 ⟩ )
32 30 30 brco ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ⟨ 𝑓 , 𝑦 ⟩ ↔ ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ∧ 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ) )
33 ancom ⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ∧ 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ) ↔ ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) )
34 5 30 brcnv ⊢ ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 )
35 3 17 5 brapply ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) )
36 34 35 bitri ⊢ ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) )
37 36 anbi1i ⊢ ( ( 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) ↔ ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) )
38 33 37 bitri ⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ∧ 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ) ↔ ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) )
39 38 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ∧ 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) )
40 fvex ⊢ ( 𝑓 ‘ 𝑦 ) ∈ V
41 breq2 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑦 ) → ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ↔ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) ( 𝑓 ‘ 𝑦 ) ) )
42 40 41 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ) ↔ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) ( 𝑓 ‘ 𝑦 ) )
43 39 42 bitri ⊢ ( ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) 𝑥 ∧ 𝑥 ◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ) ↔ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) ( 𝑓 ‘ 𝑦 ) )
44 30 40 brco ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ Restrict 𝑥 ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) )
45 3 17 5 brrestrict ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Restrict 𝑥 ↔ 𝑥 = ( 𝑓 ↾ 𝑦 ) )
46 45 anbi1i ⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ Restrict 𝑥 ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 = ( 𝑓 ↾ 𝑦 ) ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) )
47 46 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ Restrict 𝑥 ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝑓 ↾ 𝑦 ) ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) )
48 3 resex ⊢ ( 𝑓 ↾ 𝑦 ) ∈ V
49 breq1 ⊢ ( 𝑥 = ( 𝑓 ↾ 𝑦 ) → ( 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ↾ 𝑦 ) FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) )
50 48 49 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝑓 ↾ 𝑦 ) ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ↾ 𝑦 ) FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) )
51 47 50 bitri ⊢ ( ∃ 𝑥 ( ⟨ 𝑓 , 𝑦 ⟩ Restrict 𝑥 ∧ 𝑥 FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ↾ 𝑦 ) FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) )
52 48 40 brfullfun ⊢ ( ( 𝑓 ↾ 𝑦 ) FullFun 𝐹 ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
53 44 51 52 3bitri ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ Restrict ) ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
54 32 43 53 3bitri ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ⟨ 𝑓 , 𝑦 ⟩ ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
55 29 31 54 3bitri ⊢ ( 𝑓 Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) 𝑦 ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
56 55 notbii ⊢ ( ¬ 𝑓 Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) 𝑦 ↔ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
57 28 56 anbi12i ⊢ ( ( 𝑓 ( ◡ E ∘ Domain ) 𝑦 ∧ ¬ 𝑓 Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) 𝑦 ) ↔ ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
58 16 57 bitri ⊢ ( 𝑓 ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) 𝑦 ↔ ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
59 58 exbii ⊢ ( ∃ 𝑦 𝑓 ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
60 15 59 bitri ⊢ ( 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
61 df-rex ⊢ ( ∃ 𝑦 ∈ dom 𝑓 ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
62 rexnal ⊢ ( ∃ 𝑦 ∈ dom 𝑓 ¬ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ¬ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
63 60 61 62 3bitr2ri ⊢ ( ¬ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) )
64 63 con1bii ⊢ ( ¬ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ↔ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
65 14 64 anbi12i ⊢ ( ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ∧ ¬ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) ↔ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
66 anass ⊢ ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
67 65 66 bitri ⊢ ( ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ∧ ¬ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
68 eleq1 ⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ∈ On ↔ dom 𝑓 ∈ On ) )
69 raleq ⊢ ( 𝑥 = dom 𝑓 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
70 68 69 anbi12d ⊢ ( 𝑥 = dom 𝑓 → ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
71 70 anbi2d ⊢ ( 𝑥 = dom 𝑓 → ( ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ) )
72 21 71 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
73 df-fn ⊢ ( 𝑓 Fn 𝑥 ↔ ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) )
74 eqcom ⊢ ( dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓 )
75 74 anbi2i ⊢ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) ↔ ( Fun 𝑓 ∧ 𝑥 = dom 𝑓 ) )
76 ancom ⊢ ( ( Fun 𝑓 ∧ 𝑥 = dom 𝑓 ) ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) )
77 73 75 76 3bitri ⊢ ( 𝑓 Fn 𝑥 ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) )
78 77 anbi1i ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ↔ ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
79 an12 ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
80 anass ⊢ ( ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ↔ ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ) )
81 78 79 80 3bitr3ri ⊢ ( ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
82 81 exbii ⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
83 67 72 82 3bitr2i ⊢ ( ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ∧ ¬ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
84 eldif ⊢ ( 𝑓 ∈ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) ↔ ( 𝑓 ∈ ( Funs ∩ ( ◡ Domain “ On ) ) ∧ ¬ 𝑓 ∈ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) )
85 df-rex ⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
86 83 84 85 3bitr4i ⊢ ( 𝑓 ∈ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
87 86 eqabi ⊢ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
88 87 unieqi ⊢ ∪ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
89 1 88 eqtr4i ⊢ recs ( 𝐹 ) = ∪ ( ( Funs ∩ ( ◡ Domain “ On ) ) ∖ dom ( ( ◡ E ∘ Domain ) ∖ Fix ( ◡ Apply ∘ ( FullFun 𝐹 ∘ Restrict ) ) ) )