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

Theorem dfrecs2 33525
 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 7996 . 2 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 elin 3900 . . . . . . . . 9 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (𝑓 Funs 𝑓 ∈ (Domain “ On)))
3 vex 3447 . . . . . . . . . . 11 𝑓 ∈ V
43elfuns 33490 . . . . . . . . . 10 (𝑓 Funs ↔ Fun 𝑓)
5 vex 3447 . . . . . . . . . . . . . 14 𝑥 ∈ V
65, 3brcnv 5721 . . . . . . . . . . . . 13 (𝑥Domain𝑓𝑓Domain𝑥)
73, 5brdomain 33508 . . . . . . . . . . . . 13 (𝑓Domain𝑥𝑥 = dom 𝑓)
86, 7bitri 278 . . . . . . . . . . . 12 (𝑥Domain𝑓𝑥 = dom 𝑓)
98rexbii 3213 . . . . . . . . . . 11 (∃𝑥 ∈ On 𝑥Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
103elima 5905 . . . . . . . . . . 11 (𝑓 ∈ (Domain “ On) ↔ ∃𝑥 ∈ On 𝑥Domain𝑓)
11 risset 3229 . . . . . . . . . . 11 (dom 𝑓 ∈ On ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
129, 10, 113bitr4i 306 . . . . . . . . . 10 (𝑓 ∈ (Domain “ On) ↔ dom 𝑓 ∈ On)
134, 12anbi12i 629 . . . . . . . . 9 ((𝑓 Funs 𝑓 ∈ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
142, 13bitri 278 . . . . . . . 8 (𝑓 ∈ ( Funs ∩ (Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
153eldm 5737 . . . . . . . . . . 11 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16 brdif 5086 . . . . . . . . . . . . 13 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17 vex 3447 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
183, 17brco 5709 . . . . . . . . . . . . . . 15 (𝑓( E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥𝑥 E 𝑦))
197anbi1i 626 . . . . . . . . . . . . . . . . 17 ((𝑓Domain𝑥𝑥 E 𝑦) ↔ (𝑥 = dom 𝑓𝑥 E 𝑦))
2019exbii 1849 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦))
213dmex 7602 . . . . . . . . . . . . . . . . 17 dom 𝑓 ∈ V
22 breq1 5036 . . . . . . . . . . . . . . . . 17 (𝑥 = dom 𝑓 → (𝑥 E 𝑦 ↔ dom 𝑓 E 𝑦))
2321, 22ceqsexv 3492 . . . . . . . . . . . . . . . 16 (∃𝑥(𝑥 = dom 𝑓𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2420, 23bitri 278 . . . . . . . . . . . . . . 15 (∃𝑥(𝑓Domain𝑥𝑥 E 𝑦) ↔ dom 𝑓 E 𝑦)
2521, 17brcnv 5721 . . . . . . . . . . . . . . . 16 (dom 𝑓 E 𝑦𝑦 E dom 𝑓)
2621epeli 5436 . . . . . . . . . . . . . . . 16 (𝑦 E dom 𝑓𝑦 ∈ dom 𝑓)
2725, 26bitri 278 . . . . . . . . . . . . . . 15 (dom 𝑓 E 𝑦𝑦 ∈ dom 𝑓)
2818, 24, 273bitri 300 . . . . . . . . . . . . . 14 (𝑓( E ∘ Domain)𝑦𝑦 ∈ dom 𝑓)
29 df-br 5034 . . . . . . . . . . . . . . . 16 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))
30 opex 5324 . . . . . . . . . . . . . . . . 17 𝑓, 𝑦⟩ ∈ V
3130elfix 33478 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩ ∈ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
3230, 30brco 5709 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩))
33 ancom 464 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
345, 30brcnv 5721 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
353, 17, 5brapply 33513 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑓, 𝑦⟩Apply𝑥𝑥 = (𝑓𝑦))
3634, 35bitri 278 . . . . . . . . . . . . . . . . . . . . 21 (𝑥Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓𝑦))
3736anbi1i 626 . . . . . . . . . . . . . . . . . . . 20 ((𝑥Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3833, 37bitri 278 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
3938exbii 1849 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40 fvex 6662 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑦) ∈ V
41 breq2 5037 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑓𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦)))
4240, 41ceqsexv 3492 . . . . . . . . . . . . . . . . . 18 (∃𝑥(𝑥 = (𝑓𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4339, 42bitri 278 . . . . . . . . . . . . . . . . 17 (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥𝑥Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦))
4430, 40brco 5709 . . . . . . . . . . . . . . . . . 18 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)))
453, 17, 5brrestrict 33524 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑓, 𝑦⟩Restrict𝑥𝑥 = (𝑓𝑦))
4645anbi1i 626 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
4746exbii 1849 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ ∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)))
483resex 5870 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑦) ∈ V
49 breq1 5036 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑓𝑦) → (𝑥FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦)))
5048, 49ceqsexv 3492 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(𝑥 = (𝑓𝑦) ∧ 𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5147, 50bitri 278 . . . . . . . . . . . . . . . . . 18 (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥𝑥FullFun𝐹(𝑓𝑦)) ↔ (𝑓𝑦)FullFun𝐹(𝑓𝑦))
5248, 40brfullfun 33523 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑦)FullFun𝐹(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5344, 51, 523bitri 300 . . . . . . . . . . . . . . . . 17 (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓𝑦) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5432, 43, 533bitri 300 . . . . . . . . . . . . . . . 16 (⟨𝑓, 𝑦⟩(Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5529, 31, 543bitri 300 . . . . . . . . . . . . . . 15 (𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5655notbii 323 . . . . . . . . . . . . . 14 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)))
5728, 56anbi12i 629 . . . . . . . . . . . . 13 ((𝑓( E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5816, 57bitri 278 . . . . . . . . . . . 12 (𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
5958exbii 1849 . . . . . . . . . . 11 (∃𝑦 𝑓(( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
6015, 59bitri 278 . . . . . . . . . 10 (𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
61 df-rex 3115 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
62 rexnal 3204 . . . . . . . . . 10 (∃𝑦 ∈ dom 𝑓 ¬ (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6360, 61, 623bitr2ri 303 . . . . . . . . 9 (¬ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
6463con1bii 360 . . . . . . . 8 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))
6514, 64anbi12i 629 . . . . . . 7 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
66 anass 472 . . . . . . 7 (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
6765, 66bitri 278 . . . . . 6 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
68 eleq1 2880 . . . . . . . . 9 (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69 raleq 3361 . . . . . . . . 9 (𝑥 = dom 𝑓 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))
7068, 69anbi12d 633 . . . . . . . 8 (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
7170anbi2d 631 . . . . . . 7 (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
7221, 71ceqsexv 3492 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
73 df-fn 6331 . . . . . . . . . 10 (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74 eqcom 2808 . . . . . . . . . . 11 (dom 𝑓 = 𝑥𝑥 = dom 𝑓)
7574anbi2i 625 . . . . . . . . . 10 ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓𝑥 = dom 𝑓))
76 ancom 464 . . . . . . . . . 10 ((Fun 𝑓𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7773, 75, 763bitri 300 . . . . . . . . 9 (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7877anbi1i 626 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
79 an12 644 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
80 anass 472 . . . . . . . 8 (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))))
8178, 79, 803bitr3ri 305 . . . . . . 7 ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8281exbii 1849 . . . . . 6 (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8367, 72, 823bitr2i 302 . . . . 5 ((𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
84 eldif 3894 . . . . 5 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (Domain “ On)) ∧ ¬ 𝑓 ∈ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85 df-rex 3115 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
8683, 84, 853bitr4i 306 . . . 4 (𝑓 ∈ (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
8786abbi2i 2932 . . 3 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
8887unieqi 4816 . 2 (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
891, 88eqtr4i 2827 1 recs(𝐹) = (( Funs ∩ (Domain “ On)) ∖ dom (( E ∘ Domain) ∖ Fix (Apply ∘ (FullFun𝐹 ∘ Restrict))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779  ∀wral 3109  ∃wrex 3110   ∖ cdif 3881   ∩ cin 3883  ⟨cop 4534  ∪ cuni 4803   class class class wbr 5033   E cep 5432  ◡ccnv 5522  dom cdm 5523   ↾ cres 5525   “ cima 5526   ∘ ccom 5527  Oncon0 6163  Fun wfun 6322   Fn wfn 6323  ‘cfv 6328  recscrecs 7994   Fix cfix 33410   Funs cfuns 33412  Domaincdomain 33418  Applycapply 33420  FullFuncfullfn 33425  Restrictcrestrict 33426 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-symdif 4172  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fo 6334  df-fv 6336  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-txp 33429  df-pprod 33430  df-bigcup 33433  df-fix 33434  df-funs 33436  df-singleton 33437  df-singles 33438  df-image 33439  df-cart 33440  df-img 33441  df-domain 33442  df-range 33443  df-cap 33445  df-restrict 33446  df-apply 33448  df-funpart 33449  df-fullfun 33450 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator