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 abbi2i ( ( 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 ) ) ) )