Step | Hyp | Ref
| Expression |
1 | | dfrecs3 8323 |
. 2
β’
recs(πΉ) = βͺ {π
β£ βπ₯ β On
(π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))} |
2 | | elin 3931 |
. . . . . . . . 9
β’ (π β (
Funs β© (β‘Domain β
On)) β (π β Funs β§ π β (β‘Domain β On))) |
3 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
4 | 3 | elfuns 34529 |
. . . . . . . . . 10
β’ (π β
Funs β Fun π) |
5 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π₯ β V |
6 | 5, 3 | brcnv 5843 |
. . . . . . . . . . . . 13
β’ (π₯β‘Domainπ β πDomainπ₯) |
7 | 3, 5 | brdomain 34547 |
. . . . . . . . . . . . 13
β’ (πDomainπ₯ β π₯ = dom π) |
8 | 6, 7 | bitri 275 |
. . . . . . . . . . . 12
β’ (π₯β‘Domainπ β π₯ = dom π) |
9 | 8 | rexbii 3098 |
. . . . . . . . . . 11
β’
(βπ₯ β On
π₯β‘Domainπ β βπ₯ β On π₯ = dom π) |
10 | 3 | elima 6023 |
. . . . . . . . . . 11
β’ (π β (β‘Domain β On) β βπ₯ β On π₯β‘Domainπ) |
11 | | risset 3224 |
. . . . . . . . . . 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 5861 |
. . . . . . . . . . 11
β’ (π β dom ((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict))) β βπ¦
π((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict)))π¦) |
16 | | brdif 5163 |
. . . . . . . . . . . . 13
β’ (π((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict)))π¦ β (π(β‘ E β Domain)π¦ β§ Β¬ π Fix (β‘Apply β (FullFunπΉ β Restrict))π¦)) |
17 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π¦ β V |
18 | 3, 17 | brco 5831 |
. . . . . . . . . . . . . . 15
β’ (π(β‘ E β Domain)π¦ β βπ₯(πDomainπ₯ β§ π₯β‘ E
π¦)) |
19 | 7 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
β’ ((πDomainπ₯ β§ π₯β‘ E
π¦) β (π₯ = dom π β§ π₯β‘ E
π¦)) |
20 | 19 | exbii 1851 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯(πDomainπ₯ β§ π₯β‘ E
π¦) β βπ₯(π₯ = dom π β§ π₯β‘ E
π¦)) |
21 | 3 | dmex 7853 |
. . . . . . . . . . . . . . . . 17
β’ dom π β V |
22 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = dom π β (π₯β‘ E
π¦ β dom πβ‘ E π¦)) |
23 | 21, 22 | ceqsexv 3497 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯(π₯ = dom π β§ π₯β‘ E
π¦) β dom πβ‘ E π¦) |
24 | 20, 23 | bitri 275 |
. . . . . . . . . . . . . . 15
β’
(βπ₯(πDomainπ₯ β§ π₯β‘ E
π¦) β dom πβ‘ E π¦) |
25 | 21, 17 | brcnv 5843 |
. . . . . . . . . . . . . . . 16
β’ (dom
πβ‘ E π¦ β π¦ E dom π) |
26 | 21 | epeli 5544 |
. . . . . . . . . . . . . . . 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 5111 |
. . . . . . . . . . . . . . . 16
β’ (π Fix
(β‘Apply β (FullFunπΉ β Restrict))π¦ β β¨π, π¦β© β Fix
(β‘Apply β (FullFunπΉ β
Restrict))) |
30 | | opex 5426 |
. . . . . . . . . . . . . . . . 17
β’
β¨π, π¦β© β V |
31 | 30 | elfix 34517 |
. . . . . . . . . . . . . . . 16
β’
(β¨π, π¦β© β Fix (β‘Apply
β (FullFunπΉ β
Restrict)) β β¨π,
π¦β©(β‘Apply β (FullFunπΉ β Restrict))β¨π, π¦β©) |
32 | 30, 30 | brco 5831 |
. . . . . . . . . . . . . . . . 17
β’
(β¨π, π¦β©(β‘Apply β (FullFunπΉ β Restrict))β¨π, π¦β© β βπ₯(β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β§ π₯β‘Applyβ¨π, π¦β©)) |
33 | | ancom 462 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β§ π₯β‘Applyβ¨π, π¦β©) β (π₯β‘Applyβ¨π, π¦β© β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯)) |
34 | 5, 30 | brcnv 5843 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯β‘Applyβ¨π, π¦β© β β¨π, π¦β©Applyπ₯) |
35 | 3, 17, 5 | brapply 34552 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨π, π¦β©Applyπ₯ β π₯ = (πβπ¦)) |
36 | 34, 35 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯β‘Applyβ¨π, π¦β© β π₯ = (πβπ¦)) |
37 | 36 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯β‘Applyβ¨π, π¦β© β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯) β (π₯ = (πβπ¦) β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯)) |
38 | 33, 37 | bitri 275 |
. . . . . . . . . . . . . . . . . . 19
β’
((β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β§ π₯β‘Applyβ¨π, π¦β©) β (π₯ = (πβπ¦) β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯)) |
39 | 38 | exbii 1851 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ₯(β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β§ π₯β‘Applyβ¨π, π¦β©) β βπ₯(π₯ = (πβπ¦) β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯)) |
40 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . 19
β’ (πβπ¦) β V |
41 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = (πβπ¦) β (β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β β¨π, π¦β©(FullFunπΉ β Restrict)(πβπ¦))) |
42 | 40, 41 | ceqsexv 3497 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ₯(π₯ = (πβπ¦) β§ β¨π, π¦β©(FullFunπΉ β Restrict)π₯) β β¨π, π¦β©(FullFunπΉ β Restrict)(πβπ¦)) |
43 | 39, 42 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯(β¨π, π¦β©(FullFunπΉ β Restrict)π₯ β§ π₯β‘Applyβ¨π, π¦β©) β β¨π, π¦β©(FullFunπΉ β Restrict)(πβπ¦)) |
44 | 30, 40 | brco 5831 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, π¦β©(FullFunπΉ β Restrict)(πβπ¦) β βπ₯(β¨π, π¦β©Restrictπ₯ β§ π₯FullFunπΉ(πβπ¦))) |
45 | 3, 17, 5 | brrestrict 34563 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β¨π, π¦β©Restrictπ₯ β π₯ = (π βΎ π¦)) |
46 | 45 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β¨π, π¦β©Restrictπ₯ β§ π₯FullFunπΉ(πβπ¦)) β (π₯ = (π βΎ π¦) β§ π₯FullFunπΉ(πβπ¦))) |
47 | 46 | exbii 1851 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯(β¨π, π¦β©Restrictπ₯ β§ π₯FullFunπΉ(πβπ¦)) β βπ₯(π₯ = (π βΎ π¦) β§ π₯FullFunπΉ(πβπ¦))) |
48 | 3 | resex 5990 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π βΎ π¦) β V |
49 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (π βΎ π¦) β (π₯FullFunπΉ(πβπ¦) β (π βΎ π¦)FullFunπΉ(πβπ¦))) |
50 | 48, 49 | ceqsexv 3497 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯(π₯ = (π βΎ π¦) β§ π₯FullFunπΉ(πβπ¦)) β (π βΎ π¦)FullFunπΉ(πβπ¦)) |
51 | 47, 50 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ₯(β¨π, π¦β©Restrictπ₯ β§ π₯FullFunπΉ(πβπ¦)) β (π βΎ π¦)FullFunπΉ(πβπ¦)) |
52 | 48, 40 | brfullfun 34562 |
. . . . . . . . . . . . . . . . . 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 1851 |
. . . . . . . . . . 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 3075 |
. . . . . . . . . 10
β’
(βπ¦ β dom
π Β¬ (πβπ¦) = (πΉβ(π βΎ π¦)) β βπ¦(π¦ β dom π β§ Β¬ (πβπ¦) = (πΉβ(π βΎ π¦)))) |
62 | | rexnal 3104 |
. . . . . . . . . 10
β’
(βπ¦ β dom
π Β¬ (πβπ¦) = (πΉβ(π βΎ π¦)) β Β¬ βπ¦ β dom π(πβπ¦) = (πΉβ(π βΎ π¦))) |
63 | 60, 61, 62 | 3bitr2ri 300 |
. . . . . . . . 9
β’ (Β¬
βπ¦ β dom π(πβπ¦) = (πΉβ(π βΎ π¦)) β π β dom ((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict)))) |
64 | 63 | con1bii 357 |
. . . . . . . 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 470 |
. . . . . . 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 2826 |
. . . . . . . . 9
β’ (π₯ = dom π β (π₯ β On β dom π β On)) |
69 | | raleq 3312 |
. . . . . . . . 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 3497 |
. . . . . 6
β’
(βπ₯(π₯ = dom π β§ (Fun π β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))))) β (Fun π β§ (dom π β On β§ βπ¦ β dom π(πβπ¦) = (πΉβ(π βΎ π¦))))) |
73 | | df-fn 6504 |
. . . . . . . . . 10
β’ (π Fn π₯ β (Fun π β§ dom π = π₯)) |
74 | | eqcom 2744 |
. . . . . . . . . . 11
β’ (dom
π = π₯ β π₯ = dom π) |
75 | 74 | anbi2i 624 |
. . . . . . . . . 10
β’ ((Fun
π β§ dom π = π₯) β (Fun π β§ π₯ = dom π)) |
76 | | ancom 462 |
. . . . . . . . . 10
β’ ((Fun
π β§ π₯ = dom π) β (π₯ = dom π β§ Fun π)) |
77 | 73, 75, 76 | 3bitri 297 |
. . . . . . . . 9
β’ (π Fn π₯ β (π₯ = dom π β§ Fun π)) |
78 | 77 | anbi1i 625 |
. . . . . . . 8
β’ ((π Fn π₯ β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))) β ((π₯ = dom π β§ Fun π) β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))))) |
79 | | an12 644 |
. . . . . . . 8
β’ ((π Fn π₯ β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))) β (π₯ β On β§ (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))))) |
80 | | anass 470 |
. . . . . . . 8
β’ (((π₯ = dom π β§ Fun π) β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))) β (π₯ = dom π β§ (Fun π β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))))) |
81 | 78, 79, 80 | 3bitr3ri 302 |
. . . . . . 7
β’ ((π₯ = dom π β§ (Fun π β§ (π₯ β On β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))))) β (π₯ β On β§ (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦))))) |
82 | 81 | exbii 1851 |
. . . . . 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 3925 |
. . . . 5
β’ (π β ((
Funs β© (β‘Domain β
On)) β dom ((β‘ E β Domain)
β Fix (β‘Apply β (FullFunπΉ β Restrict)))) β (π β (
Funs β© (β‘Domain β
On)) β§ Β¬ π β
dom ((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict))))) |
85 | | df-rex 3075 |
. . . . 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 | abbi2i 2874 |
. . 3
β’ (( Funs β© (β‘Domain β On)) β dom ((β‘ E β Domain) β Fix (β‘Apply
β (FullFunπΉ β
Restrict)))) = {π β£
βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))} |
88 | 87 | unieqi 4883 |
. 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)))) |