| Step | Hyp | Ref
| Expression |
| 1 | | dfrecs3 8412 |
. 2
⊢
recs(𝐹) = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| 2 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On))) |
| 3 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
| 4 | 3 | elfuns 35916 |
. . . . . . . . . 10
⊢ (𝑓 ∈
Funs ↔ Fun 𝑓) |
| 5 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 6 | 5, 3 | brcnv 5893 |
. . . . . . . . . . . . 13
⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥) |
| 7 | 3, 5 | brdomain 35934 |
. . . . . . . . . . . . 13
⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓) |
| 8 | 6, 7 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓) |
| 9 | 8 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ On
𝑥◡Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓) |
| 10 | 3 | elima 6083 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓) |
| 11 | | risset 3233 |
. . . . . . . . . . 11
⊢ (dom
𝑓 ∈ On ↔
∃𝑥 ∈ On 𝑥 = dom 𝑓) |
| 12 | 9, 10, 11 | 3bitr4i 303 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On) |
| 13 | 4, 12 | anbi12i 628 |
. . . . . . . . 9
⊢ ((𝑓 ∈
Funs ∧ 𝑓 ∈
(◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On)) |
| 14 | 2, 13 | bitri 275 |
. . . . . . . 8
⊢ (𝑓 ∈ (
Funs ∩ (◡Domain “
On)) ↔ (Fun 𝑓 ∧
dom 𝑓 ∈
On)) |
| 15 | 3 | eldm 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 |
| 18 | 3, 17 | brco 5881 |
. . . . . . . . . . . . . . 15
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦)) |
| 19 | 7 | anbi1i 624 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
| 20 | 19 | exbii 1848 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦)) |
| 21 | 3 | dmex 7931 |
. . . . . . . . . . . . . . . . 17
⊢ dom 𝑓 ∈ V |
| 22 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = dom 𝑓 → (𝑥◡ E
𝑦 ↔ dom 𝑓◡ E 𝑦)) |
| 23 | 21, 22 | ceqsexv 3532 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
| 24 | 20, 23 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E
𝑦) ↔ dom 𝑓◡ E 𝑦) |
| 25 | 21, 17 | brcnv 5893 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓) |
| 26 | 21 | epeli 5586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓) |
| 27 | 25, 26 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓) |
| 28 | 18, 24, 27 | 3bitri 297 |
. . . . . . . . . . . . . 14
⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓) |
| 29 | | df-br 5144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fix
(◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ 〈𝑓, 𝑦〉 ∈ Fix
(◡Apply ∘ (FullFun𝐹 ∘
Restrict))) |
| 30 | | opex 5469 |
. . . . . . . . . . . . . . . . 17
⊢
〈𝑓, 𝑦〉 ∈ V |
| 31 | 30 | elfix 35904 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑓, 𝑦〉 ∈ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)) ↔ 〈𝑓,
𝑦〉(◡Apply ∘ (FullFun𝐹 ∘ Restrict))〈𝑓, 𝑦〉) |
| 32 | 30, 30 | brco 5881 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑓, 𝑦〉(◡Apply ∘ (FullFun𝐹 ∘ Restrict))〈𝑓, 𝑦〉 ↔ ∃𝑥(〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply〈𝑓, 𝑦〉)) |
| 33 | | ancom 460 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥◡Apply〈𝑓, 𝑦〉 ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥)) |
| 34 | 5, 30 | brcnv 5893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 〈𝑓, 𝑦〉Apply𝑥) |
| 35 | 3, 17, 5 | brapply 35939 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑓, 𝑦〉Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦)) |
| 36 | 34, 35 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥◡Apply〈𝑓, 𝑦〉 ↔ 𝑥 = (𝑓‘𝑦)) |
| 37 | 36 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥◡Apply〈𝑓, 𝑦〉 ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓‘𝑦) ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥)) |
| 38 | 33, 37 | bitri 275 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply〈𝑓, 𝑦〉) ↔ (𝑥 = (𝑓‘𝑦) ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥)) |
| 39 | 38 | exbii 1848 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply〈𝑓, 𝑦〉) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥)) |
| 40 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓‘𝑦) ∈ V |
| 41 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑓‘𝑦) → (〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ↔ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))) |
| 42 | 40, 41 | ceqsexv 3532 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥) ↔ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)) |
| 43 | 39, 42 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply〈𝑓, 𝑦〉) ↔ 〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)) |
| 44 | 30, 40 | brco 5881 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ ∃𝑥(〈𝑓, 𝑦〉Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦))) |
| 45 | 3, 17, 5 | brrestrict 35950 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑓, 𝑦〉Restrict𝑥 ↔ 𝑥 = (𝑓 ↾ 𝑦)) |
| 46 | 45 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑓, 𝑦〉Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦))) |
| 47 | 46 | exbii 1848 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥(〈𝑓, 𝑦〉Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ ∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦))) |
| 48 | 3 | resex 6047 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ↾ 𝑦) ∈ V |
| 49 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑓 ↾ 𝑦) → (𝑥FullFun𝐹(𝑓‘𝑦) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))) |
| 50 | 48, 49 | ceqsexv 3532 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)) |
| 51 | 47, 50 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(〈𝑓, 𝑦〉Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)) |
| 52 | 48, 40 | brfullfun 35949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 53 | 44, 51, 52 | 3bitri 297 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑓, 𝑦〉(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 54 | 32, 43, 53 | 3bitri 297 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑓, 𝑦〉(◡Apply ∘ (FullFun𝐹 ∘ Restrict))〈𝑓, 𝑦〉 ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 55 | 29, 31, 54 | 3bitri 297 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fix
(◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 56 | 55 | notbii 320 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑓 Fix
(◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 57 | 28, 56 | anbi12i 628 |
. . . . . . . . . . . . 13
⊢ ((𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 58 | 16, 57 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 59 | 58 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))𝑦 ↔
∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 60 | 15, 59 | bitri 275 |
. . . . . . . . . 10
⊢ (𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 61 | | df-rex 3071 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ dom
𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 62 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ dom
𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 63 | 60, 61, 62 | 3bitr2ri 300 |
. . . . . . . . 9
⊢ (¬
∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))) |
| 64 | 63 | con1bii 356 |
. . . . . . . 8
⊢ (¬
𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) |
| 65 | 14, 64 | anbi12i 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 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 67 | 65, 66 | bitri 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 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 70 | 68, 69 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 71 | 70 | anbi2d 630 |
. . . . . . 7
⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))) |
| 72 | 21, 71 | ceqsexv 3532 |
. . . . . 6
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 73 | | df-fn 6564 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥)) |
| 74 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓) |
| 75 | 74 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓 ∧ 𝑥 = dom 𝑓)) |
| 76 | | ancom 460 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ 𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
| 77 | 73, 75, 76 | 3bitri 297 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓)) |
| 78 | 77 | anbi1i 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 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))) |
| 81 | 78, 79, 80 | 3bitr3ri 302 |
. . . . . . 7
⊢ ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 82 | 81 | exbii 1848 |
. . . . . 6
⊢
(∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 83 | 67, 72, 82 | 3bitr2i 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 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
| 86 | 83, 84, 85 | 3bitr4i 303 |
. . . 4
⊢ (𝑓 ∈ ((
Funs ∩ (◡Domain “
On)) ∖ dom ((◡ E ∘ Domain)
∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
| 87 | 86 | eqabi 2877 |
. . 3
⊢ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))) = {𝑓 ∣
∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| 88 | 87 | unieqi 4919 |
. 2
⊢ ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
| 89 | 1, 88 | eqtr4i 2768 |
1
⊢
recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply
∘ (FullFun𝐹 ∘
Restrict)))) |