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

Theorem dfrecs2 35951
Description: A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)
Assertion
Ref Expression
dfrecs2 recs(𝐹) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))

Proof of Theorem dfrecs2
Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrecs3 8412 . 2 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 elin 3967 . . . . . . . . 9 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
3 vex 3484 . . . . . . . . . . 11 𝑓 ∈ V
43elfuns 35916 . . . . . . . . . 10 (𝑓 Funs ↔ Fun 𝑓)
5 vex 3484 . . . . . . . . . . . . . 14 𝑥 ∈ V
65, 3brcnv 5893 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑓Domain𝑥)
73, 5brdomain 35934 . . . . . . . . . . . . 13 (𝑓Domain𝑥𝑥 = dom 𝑓)
86, 7bitri 275 . . . . . . . . . . . 12 (𝑥Domain𝑓𝑥 = dom 𝑓)
98rexbii 3094 . . . . . . . . . . 11 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
103elima 6083 . . . . . . . . . . 11 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
11 risset 3233 . . . . . . . . . . 11 (dom 𝑓 ∈ On ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
129, 10, 113bitr4i 303 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
134, 12anbi12i 628 . . . . . . . . 9 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
142, 13bitri 275 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
153eldm 5911 . . . . . . . . . . 11 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16 brdif 5196 . . . . . . . . . . . . 13 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17 vex 3484 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
183, 17brco 5881 . . . . . . . . . . . . . . 15 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
197anbi1i 624 . . . . . . . . . . . . . . . . 17 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
2019exbii 1848 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
213dmex 7931 . . . . . . . . . . . . . . . . 17 dom 𝑓 ∈ V
22 breq1 5146 . . . . . . . . . . . . . . . . 17 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
2321, 22ceqsexv 3532 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2420, 23bitri 275 . . . . . . . . . . . . . . 15 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2521, 17brcnv 5893 . . . . . . . . . . . . . . . 16 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
2621epeli 5586 . . . . . . . . . . . . . . . 16 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
2725, 26bitri 275 . . . . . . . . . . . . . . 15 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
2818, 24, 273bitri 297 . . . . . . . . . . . . . 14 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
29 df-br 5144 . . . . . . . . . . . . . . . 16 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))
30 opex 5469 . . . . . . . . . . . . . . . . 17 𝑓, 𝑦⟩ ∈ V
3130elfix 35904 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
3230, 30brco 5881 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩))
33 ancom 460 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
345, 30brcnv 5893 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
353, 17, 5brapply 35939 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
3634, 35bitri 275 . . . . . . . . . . . . . . . . . . . . 21 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
3736anbi1i 624 . . . . . . . . . . . . . . . . . . . 20 ((𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3833, 37bitri 275 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3938exbii 1848 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40 fvex 6919 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑦) ∈ V
41 breq2 5147 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦)))
4240, 41ceqsexv 3532 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4339, 42bitri 275 . . . . . . . . . . . . . . . . 17 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4430, 40brco 5881 . . . . . . . . . . . . . . . . . 18 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)))
453, 17, 5brrestrict 35950 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑓, 𝑦⟩Restrict𝑥𝑥 = (𝑓𝑦))
4645anbi1i 624 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
4746exbii 1848 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
483resex 6047 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
49 breq1 5146 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓𝑦) → (𝑥FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦)))
5048, 49ceqsexv 3532 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5147, 50bitri 275 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5248, 40brfullfun 35949 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑦)FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5344, 51, 523bitri 297 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5432, 43, 533bitri 297 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5529, 31, 543bitri 297 . . . . . . . . . . . . . . 15 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5655notbii 320 . . . . . . . . . . . . . 14 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5728, 56anbi12i 628 . . . . . . . . . . . . 13 ((𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5816, 57bitri 275 . . . . . . . . . . . 12 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5958exbii 1848 . . . . . . . . . . 11 (∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
6015, 59bitri 275 . . . . . . . . . 10 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
61 df-rex 3071 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
62 rexnal 3100 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6360, 61, 623bitr2ri 300 . . . . . . . . 9 (¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
6463con1bii 356 . . . . . . . 8 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6514, 64anbi12i 628 . . . . . . 7 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
66 anass 468 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
6765, 66bitri 275 . . . . . 6 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
68 eleq1 2829 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69 raleq 3323 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
7068, 69anbi12d 632 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
7170anbi2d 630 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
7221, 71ceqsexv 3532 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
73 df-fn 6564 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74 eqcom 2744 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
7574anbi2i 623 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓𝑥 = dom 𝑓))
76 ancom 460 . . . . . . . . . 10 ((Fun 𝑓𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7773, 75, 763bitri 297 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7877anbi1i 624 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
79 an12 645 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
80 anass 468 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
8178, 79, 803bitr3ri 302 . . . . . . 7 ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8281exbii 1848 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8367, 72, 823bitr2i 299 . . . . 5 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
84 eldif 3961 . . . . 5 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85 df-rex 3071 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8683, 84, 853bitr4i 303 . . . 4 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
8786eqabi 2877 . . 3 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
8887unieqi 4919 . 2 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
891, 88eqtr4i 2768 1 recs(𝐹) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070  cdif 3948  cin 3950  cop 4632   cuni 4907   class class class wbr 5143   E cep 5583  ccnv 5684  dom cdm 5685  cres 5687  cima 5688  ccom 5689  Oncon0 6384  Fun wfun 6555   Fn wfn 6556  cfv 6561  recscrecs 8410   Fix cfix 35836   Funs cfuns 35838  Domaincdomain 35844  Applycapply 35846  FullFuncfullfn 35851  Restrictcrestrict 35852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-symdif 4253  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fo 6567  df-fv 6569  df-ov 7434  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-txp 35855  df-pprod 35856  df-bigcup 35859  df-fix 35860  df-funs 35862  df-singleton 35863  df-singles 35864  df-image 35865  df-cart 35866  df-img 35867  df-domain 35868  df-range 35869  df-cap 35871  df-restrict 35872  df-apply 35874  df-funpart 35875  df-fullfun 35876
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator