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 32334
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 7626 . 2 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 elin 3927 . . . . . . . . 9 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
3 vex 3331 . . . . . . . . . . 11 𝑓 ∈ V
43elfuns 32299 . . . . . . . . . 10 (𝑓 Funs ↔ Fun 𝑓)
5 vex 3331 . . . . . . . . . . . . . 14 𝑥 ∈ V
65, 3brcnv 5448 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑓Domain𝑥)
73, 5brdomain 32317 . . . . . . . . . . . . 13 (𝑓Domain𝑥𝑥 = dom 𝑓)
86, 7bitri 264 . . . . . . . . . . . 12 (𝑥Domain𝑓𝑥 = dom 𝑓)
98rexbii 3167 . . . . . . . . . . 11 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
103elima 5617 . . . . . . . . . . 11 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
11 risset 3188 . . . . . . . . . . 11 (dom 𝑓 ∈ On ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
129, 10, 113bitr4i 292 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
134, 12anbi12i 735 . . . . . . . . 9 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
142, 13bitri 264 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
153eldm 5464 . . . . . . . . . . 11 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16 brdif 4845 . . . . . . . . . . . . 13 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17 vex 3331 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
183, 17brco 5436 . . . . . . . . . . . . . . 15 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
197anbi1i 733 . . . . . . . . . . . . . . . . 17 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
2019exbii 1911 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
213dmex 7252 . . . . . . . . . . . . . . . . 17 dom 𝑓 ∈ V
22 breq1 4795 . . . . . . . . . . . . . . . . 17 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
2321, 22ceqsexv 3370 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2420, 23bitri 264 . . . . . . . . . . . . . . 15 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2521, 17brcnv 5448 . . . . . . . . . . . . . . . 16 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
2621epelc 5169 . . . . . . . . . . . . . . . 16 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
2725, 26bitri 264 . . . . . . . . . . . . . . 15 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
2818, 24, 273bitri 286 . . . . . . . . . . . . . 14 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
29 df-br 4793 . . . . . . . . . . . . . . . 16 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))
30 opex 5069 . . . . . . . . . . . . . . . . 17 𝑓, 𝑦⟩ ∈ V
3130elfix 32287 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
3230, 30brco 5436 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩))
33 ancom 465 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
345, 30brcnv 5448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
353, 17, 5brapply 32322 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
3634, 35bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
3736anbi1i 733 . . . . . . . . . . . . . . . . . . . 20 ((𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3833, 37bitri 264 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3938exbii 1911 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40 fvex 6350 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑦) ∈ V
41 breq2 4796 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦)))
4240, 41ceqsexv 3370 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4339, 42bitri 264 . . . . . . . . . . . . . . . . 17 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4430, 40brco 5436 . . . . . . . . . . . . . . . . . 18 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)))
453, 17, 5brrestrict 32333 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑓, 𝑦⟩Restrict𝑥𝑥 = (𝑓𝑦))
4645anbi1i 733 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
4746exbii 1911 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
483resex 5589 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
49 breq1 4795 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓𝑦) → (𝑥FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦)))
5048, 49ceqsexv 3370 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5147, 50bitri 264 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5248, 40brfullfun 32332 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑦)FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5344, 51, 523bitri 286 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5432, 43, 533bitri 286 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5529, 31, 543bitri 286 . . . . . . . . . . . . . . 15 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5655notbii 309 . . . . . . . . . . . . . 14 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5728, 56anbi12i 735 . . . . . . . . . . . . 13 ((𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5816, 57bitri 264 . . . . . . . . . . . 12 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5958exbii 1911 . . . . . . . . . . 11 (∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
6015, 59bitri 264 . . . . . . . . . 10 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
61 df-rex 3044 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
62 rexnal 3121 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6360, 61, 623bitr2ri 289 . . . . . . . . 9 (¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
6463con1bii 345 . . . . . . . 8 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6514, 64anbi12i 735 . . . . . . 7 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
66 anass 684 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
6765, 66bitri 264 . . . . . 6 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
68 eleq1 2815 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69 raleq 3265 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
7068, 69anbi12d 749 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
7170anbi2d 742 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
7221, 71ceqsexv 3370 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
73 df-fn 6040 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74 eqcom 2755 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
7574anbi2i 732 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓𝑥 = dom 𝑓))
76 ancom 465 . . . . . . . . . 10 ((Fun 𝑓𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7773, 75, 763bitri 286 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7877anbi1i 733 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
79 an12 873 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
80 anass 684 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
8178, 79, 803bitr3ri 291 . . . . . . 7 ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8281exbii 1911 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8367, 72, 823bitr2i 288 . . . . 5 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
84 eldif 3713 . . . . 5 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85 df-rex 3044 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8683, 84, 853bitr4i 292 . . . 4 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
8786abbi2i 2864 . . 3 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
8887unieqi 4585 . 2 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
891, 88eqtr4i 2773 1 recs(𝐹) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 383   = wceq 1620  wex 1841  wcel 2127  {cab 2734  wral 3038  wrex 3039  cdif 3700  cin 3702  cop 4315   cuni 4576   class class class wbr 4792   E cep 5166  ccnv 5253  dom cdm 5254  cres 5256  cima 5257  ccom 5258  Oncon0 5872  Fun wfun 6031   Fn wfn 6032  cfv 6037  recscrecs 7624   Fix cfix 32219   Funs cfuns 32221  Domaincdomain 32227  Applycapply 32229  FullFuncfullfn 32234  Restrictcrestrict 32235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-symdif 3975  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-fo 6043  df-fv 6045  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-txp 32238  df-pprod 32239  df-bigcup 32242  df-fix 32243  df-funs 32245  df-singleton 32246  df-singles 32247  df-image 32248  df-cart 32249  df-img 32250  df-domain 32251  df-range 32252  df-cap 32254  df-restrict 32255  df-apply 32257  df-funpart 32258  df-fullfun 32259
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator