Step | Hyp | Ref
| Expression |
1 | | elequ2 2122 |
. . . . . . 7
β’ (β = π β (π β β β π β π)) |
2 | | elequ2 2122 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
3 | 2 | notbid 318 |
. . . . . . 7
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
4 | 1, 3 | bi2anan9r 639 |
. . . . . 6
β’ ((π = π β§ β = π) β ((π β β β§ Β¬ π β π) β (π β π β§ Β¬ π β π))) |
5 | | elequ2 2122 |
. . . . . . . . 9
β’ (π = π β (π β π β π β π)) |
6 | | elequ2 2122 |
. . . . . . . . 9
β’ (β = π β (π β β β π β π)) |
7 | 5, 6 | bi2bian9 640 |
. . . . . . . 8
β’ ((π = π β§ β = π) β ((π β π β π β β) β (π β π β π β π))) |
8 | 7 | imbi2d 341 |
. . . . . . 7
β’ ((π = π β§ β = π) β ((π(πββͺ dom π)π β (π β π β π β β)) β (π(πββͺ dom π)π β (π β π β π β π)))) |
9 | 8 | ralbidv 3175 |
. . . . . 6
β’ ((π = π β§ β = π) β (βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)) β βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)))) |
10 | 4, 9 | anbi12d 632 |
. . . . 5
β’ ((π = π β§ β = π) β (((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))) β ((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))))) |
11 | 10 | rexbidv 3176 |
. . . 4
β’ ((π = π β§ β = π) β (βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))) β βπ β (π
1ββͺ dom π)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))))) |
12 | | elequ1 2114 |
. . . . . . 7
β’ (π = π β (π β π β π β π)) |
13 | | elequ1 2114 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
14 | 13 | notbid 318 |
. . . . . . 7
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
15 | 12, 14 | anbi12d 632 |
. . . . . 6
β’ (π = π β ((π β π β§ Β¬ π β π) β (π β π β§ Β¬ π β π))) |
16 | | breq2 5114 |
. . . . . . . . 9
β’ (π = π β (π(πββͺ dom π)π β π(πββͺ dom π)π)) |
17 | 16 | imbi1d 342 |
. . . . . . . 8
β’ (π = π β ((π(πββͺ dom π)π β (π β π β π β π)) β (π(πββͺ dom π)π β (π β π β π β π)))) |
18 | 17 | ralbidv 3175 |
. . . . . . 7
β’ (π = π β (βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)) β βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)))) |
19 | | breq1 5113 |
. . . . . . . . 9
β’ (π = π β (π(πββͺ dom π)π β π(πββͺ dom π)π)) |
20 | | elequ1 2114 |
. . . . . . . . . 10
β’ (π = π β (π β π β π β π)) |
21 | | elequ1 2114 |
. . . . . . . . . 10
β’ (π = π β (π β π β π β π)) |
22 | 20, 21 | bibi12d 346 |
. . . . . . . . 9
β’ (π = π β ((π β π β π β π) β (π β π β π β π))) |
23 | 19, 22 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((π(πββͺ dom π)π β (π β π β π β π)) β (π(πββͺ dom π)π β (π β π β π β π)))) |
24 | 23 | cbvralvw 3228 |
. . . . . . 7
β’
(βπ β
(π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)) β βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))) |
25 | 18, 24 | bitrdi 287 |
. . . . . 6
β’ (π = π β (βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)) β βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)))) |
26 | 15, 25 | anbi12d 632 |
. . . . 5
β’ (π = π β (((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))) β ((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))))) |
27 | 26 | cbvrexvw 3229 |
. . . 4
β’
(βπ β
(π
1ββͺ dom π)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))) β βπ β (π
1ββͺ dom π)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)))) |
28 | 11, 27 | bitrdi 287 |
. . 3
β’ ((π = π β§ β = π) β (βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))) β βπ β (π
1ββͺ dom π)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π))))) |
29 | 28 | cbvopabv 5183 |
. 2
β’
{β¨π, ββ© β£ βπ β
(π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))} = {β¨π, πβ© β£ βπ β (π
1ββͺ dom π)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β π)))} |
30 | | nfcv 2908 |
. . 3
β’
β²πsup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) |
31 | | nfcv 2908 |
. . . 4
β’
β²π(π¦βπ) |
32 | | nfcv 2908 |
. . . 4
β’
β²π(π
1βdom π) |
33 | | nfopab1 5180 |
. . . 4
β’
β²π{β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))} |
34 | 31, 32, 33 | nfsup 9394 |
. . 3
β’
β²πsup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) |
35 | | fveq2 6847 |
. . . 4
β’ (π = π β (π¦βπ) = (π¦βπ)) |
36 | 35 | supeq1d 9389 |
. . 3
β’ (π = π β sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) = sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) |
37 | 30, 34, 36 | cbvmpt 5221 |
. 2
β’ (π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) = (π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) |
38 | | nfcv 2908 |
. . . 4
β’
β²π((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)) |
39 | | nffvmpt1 6858 |
. . . 4
β’
β²π((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)) |
40 | | rneq 5896 |
. . . . . 6
β’ (π = π β ran π = ran π) |
41 | 40 | difeq2d 4087 |
. . . . 5
β’ (π = π β ((π
1βdom
π) β ran π) =
((π
1βdom π) β ran π)) |
42 | 41 | fveq2d 6851 |
. . . 4
β’ (π = π β ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)) = ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) |
43 | 38, 39, 42 | cbvmpt 5221 |
. . 3
β’ (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) = (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) |
44 | | recseq 8325 |
. . 3
β’ ((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) = (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) β recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) = recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))))) |
45 | 43, 44 | ax-mp 5 |
. 2
β’
recs((π β V
β¦ ((π β V
β¦ sup((π¦βπ),
(π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) = recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
46 | | nfv 1918 |
. . 3
β’
β²πβ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) |
47 | | nfv 1918 |
. . 3
β’
β²πβ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) |
48 | | nfmpt1 5218 |
. . . . . . . 8
β’
β²π(π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) |
49 | 48 | nfrecs 8326 |
. . . . . . 7
β’
β²πrecs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
50 | 49 | nfcnv 5839 |
. . . . . 6
β’
β²πβ‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
51 | | nfcv 2908 |
. . . . . 6
β’
β²π{π} |
52 | 50, 51 | nfima 6026 |
. . . . 5
β’
β²π(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
53 | 52 | nfint 4922 |
. . . 4
β’
β²πβ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
54 | | nfcv 2908 |
. . . . . 6
β’
β²π{π} |
55 | 50, 54 | nfima 6026 |
. . . . 5
β’
β²π(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
56 | 55 | nfint 4922 |
. . . 4
β’
β²πβ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
57 | 53, 56 | nfel 2922 |
. . 3
β’
β²πβ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
58 | | nfcv 2908 |
. . . . . . . . 9
β’
β²βV |
59 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²β(π¦βπ) |
60 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²β(π
1βdom π) |
61 | | nfopab2 5181 |
. . . . . . . . . . . 12
β’
β²β{β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))} |
62 | 59, 60, 61 | nfsup 9394 |
. . . . . . . . . . 11
β’
β²βsup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) |
63 | 58, 62 | nfmpt 5217 |
. . . . . . . . . 10
β’
β²β(π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) |
64 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²β((π
1βdom π) β ran π) |
65 | 63, 64 | nffv 6857 |
. . . . . . . . 9
β’
β²β((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)) |
66 | 58, 65 | nfmpt 5217 |
. . . . . . . 8
β’
β²β(π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) |
67 | 66 | nfrecs 8326 |
. . . . . . 7
β’
β²βrecs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
68 | 67 | nfcnv 5839 |
. . . . . 6
β’
β²ββ‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
69 | | nfcv 2908 |
. . . . . 6
β’
β²β{π} |
70 | 68, 69 | nfima 6026 |
. . . . 5
β’
β²β(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
71 | 70 | nfint 4922 |
. . . 4
β’
β²ββ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
72 | | nfcv 2908 |
. . . . . 6
β’
β²β{π} |
73 | 68, 72 | nfima 6026 |
. . . . 5
β’
β²β(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
74 | 73 | nfint 4922 |
. . . 4
β’
β²ββ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
75 | 71, 74 | nfel 2922 |
. . 3
β’
β²ββ© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) |
76 | | sneq 4601 |
. . . . . 6
β’ (π = π β {π} = {π}) |
77 | 76 | imaeq2d 6018 |
. . . . 5
β’ (π = π β (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) = (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
78 | 77 | inteqd 4917 |
. . . 4
β’ (π = π β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
79 | | sneq 4601 |
. . . . . 6
β’ (β = π β {β} = {π}) |
80 | 79 | imaeq2d 6018 |
. . . . 5
β’ (β = π β (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) = (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
81 | 80 | inteqd 4917 |
. . . 4
β’ (β = π β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
82 | | eleq12 2828 |
. . . 4
β’ ((β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β§ β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) β (β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}))) |
83 | 78, 81, 82 | syl2an 597 |
. . 3
β’ ((π = π β§ β = π) β (β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}))) |
84 | 46, 47, 57, 75, 83 | cbvopab 5182 |
. 2
β’
{β¨π, ββ© β£ β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})} = {β¨π, πβ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})} |
85 | | fveq2 6847 |
. . . . 5
β’ (π = π β (rankβπ) = (rankβπ)) |
86 | | fveq2 6847 |
. . . . 5
β’ (β = π β (rankββ) = (rankβπ)) |
87 | 85, 86 | breqan12d 5126 |
. . . 4
β’ ((π = π β§ β = π) β ((rankβπ) E (rankββ) β (rankβπ) E (rankβπ))) |
88 | 85, 86 | eqeqan12d 2751 |
. . . . 5
β’ ((π = π β§ β = π) β ((rankβπ) = (rankββ) β (rankβπ) = (rankβπ))) |
89 | | simpl 484 |
. . . . . 6
β’ ((π = π β§ β = π) β π = π) |
90 | | suceq 6388 |
. . . . . . . . 9
β’
((rankβπ) =
(rankβπ) β suc
(rankβπ) = suc
(rankβπ)) |
91 | 85, 90 | syl 17 |
. . . . . . . 8
β’ (π = π β suc (rankβπ) = suc (rankβπ)) |
92 | 91 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ β = π) β suc (rankβπ) = suc (rankβπ)) |
93 | 92 | fveq2d 6851 |
. . . . . 6
β’ ((π = π β§ β = π) β (πβsuc (rankβπ)) = (πβsuc (rankβπ))) |
94 | | simpr 486 |
. . . . . 6
β’ ((π = π β§ β = π) β β = π) |
95 | 89, 93, 94 | breq123d 5124 |
. . . . 5
β’ ((π = π β§ β = π) β (π(πβsuc (rankβπ))β β π(πβsuc (rankβπ))π)) |
96 | 88, 95 | anbi12d 632 |
. . . 4
β’ ((π = π β§ β = π) β (((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β) β ((rankβπ) = (rankβπ) β§ π(πβsuc (rankβπ))π))) |
97 | 87, 96 | orbi12d 918 |
. . 3
β’ ((π = π β§ β = π) β (((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β)) β ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(πβsuc (rankβπ))π)))) |
98 | 97 | cbvopabv 5183 |
. 2
β’
{β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))} = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(πβsuc (rankβπ))π))} |
99 | | eqid 2737 |
. 2
β’ (if(dom
π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))) = (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))) |
100 | | dmeq 5864 |
. . . . . . 7
β’ (π = π β dom π = dom π) |
101 | 100 | unieqd 4884 |
. . . . . . 7
β’ (π = π β βͺ dom
π = βͺ dom π) |
102 | 100, 101 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (dom π = βͺ dom π β dom π = βͺ dom π)) |
103 | | fveq1 6846 |
. . . . . . . . . 10
β’ (π = π β (πβsuc (rankβπ)) = (πβsuc (rankβπ))) |
104 | 103 | breqd 5121 |
. . . . . . . . 9
β’ (π = π β (π(πβsuc (rankβπ))β β π(πβsuc (rankβπ))β)) |
105 | 104 | anbi2d 630 |
. . . . . . . 8
β’ (π = π β (((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β) β ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))) |
106 | 105 | orbi2d 915 |
. . . . . . 7
β’ (π = π β (((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β)) β ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β)))) |
107 | 106 | opabbidv 5176 |
. . . . . 6
β’ (π = π β {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))} = {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}) |
108 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π¦βπ) = (π¦βπ)) |
109 | 100 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π
1βdom
π) =
(π
1βdom π)) |
110 | 101 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π
1ββͺ dom π) = (π
1ββͺ dom π)) |
111 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β π = π) |
112 | 111, 101 | fveq12d 6854 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πββͺ dom π) = (πββͺ dom π)) |
113 | 112 | breqd 5121 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π(πββͺ dom π)π β π(πββͺ dom π)π)) |
114 | 113 | imbi1d 342 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π(πββͺ dom π)π β (π β π β π β β)) β (π(πββͺ dom π)π β (π β π β π β β)))) |
115 | 110, 114 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)) β βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))) |
116 | 115 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))) β ((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))))) |
117 | 110, 116 | rexeqbidv 3323 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))) β βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β))))) |
118 | 117 | opabbidv 5176 |
. . . . . . . . . . . . . . . 16
β’ (π = π β {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))} = {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) |
119 | 108, 109,
118 | supeq123d 9393 |
. . . . . . . . . . . . . . 15
β’ (π = π β sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}) = sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) |
120 | 119 | mpteq2dv 5212 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))})) = (π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))) |
121 | 109 | difeq1d 4086 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π
1βdom
π) β ran π) =
((π
1βdom π) β ran π)) |
122 | 120, 121 | fveq12d 6854 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)) = ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) |
123 | 122 | mpteq2dv 5212 |
. . . . . . . . . . . 12
β’ (π = π β (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) = (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) |
124 | | recseq 8325 |
. . . . . . . . . . . 12
β’ ((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) = (π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))) β recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) = recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))))) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . 11
β’ (π = π β recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) = recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))))) |
126 | 125 | cnveqd 5836 |
. . . . . . . . . 10
β’ (π = π β β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) = β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π))))) |
127 | 126 | imaeq1d 6017 |
. . . . . . . . 9
β’ (π = π β (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) = (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
128 | 127 | inteqd 4917 |
. . . . . . . 8
β’ (π = π β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π})) |
129 | 126 | imaeq1d 6017 |
. . . . . . . . 9
β’ (π = π β (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) = (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})) |
130 | 129 | inteqd 4917 |
. . . . . . . 8
β’ (π = π β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) = β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})) |
131 | 128, 130 | eleq12d 2832 |
. . . . . . 7
β’ (π = π β (β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β}))) |
132 | 131 | opabbidv 5176 |
. . . . . 6
β’ (π = π β {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})} = {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) |
133 | 102, 107,
132 | ifbieq12d 4519 |
. . . . 5
β’ (π = π β if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) = if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})})) |
134 | 109 | sqxpeqd 5670 |
. . . . 5
β’ (π = π β ((π
1βdom
π) Γ
(π
1βdom π)) = ((π
1βdom π) Γ
(π
1βdom π))) |
135 | 133, 134 | ineq12d 4178 |
. . . 4
β’ (π = π β (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))) = (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))) |
136 | 135 | cbvmptv 5223 |
. . 3
β’ (π β V β¦ (if(dom π = βͺ
dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))) = (π β V β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))) |
137 | | recseq 8325 |
. . 3
β’ ((π β V β¦ (if(dom π = βͺ
dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))) = (π β V β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))) β recs((π β V β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))))) = recs((π β V β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π)))))) |
138 | 136, 137 | ax-mp 5 |
. 2
β’
recs((π β V
β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))))) = recs((π β V β¦ (if(dom π = βͺ dom π, {β¨π, ββ© β£ ((rankβπ) E (rankββ) β¨ ((rankβπ) = (rankββ) β§ π(πβsuc (rankβπ))β))}, {β¨π, ββ© β£ β©
(β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {π}) β β© (β‘recs((π β V β¦ ((π β V β¦ sup((π¦βπ), (π
1βdom π), {β¨π, ββ© β£ βπ β (π
1ββͺ dom π)((π β β β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π)(π(πββͺ dom π)π β (π β π β π β β)))}))β((π
1βdom
π) β ran π)))) β {β})}) β© ((π
1βdom
π) Γ
(π
1βdom π))))) |
139 | | aomclem8.a |
. 2
β’ (π β π΄ β On) |
140 | | aomclem8.y |
. . 3
β’ (π β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
141 | | neeq1 3007 |
. . . . 5
β’ (π = π β (π β β
β π β β
)) |
142 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (π¦βπ) = (π¦βπ)) |
143 | | pweq 4579 |
. . . . . . . 8
β’ (π = π β π« π = π« π) |
144 | 143 | ineq1d 4176 |
. . . . . . 7
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
145 | 144 | difeq1d 4086 |
. . . . . 6
β’ (π = π β ((π« π β© Fin) β {β
}) = ((π«
π β© Fin) β
{β
})) |
146 | 142, 145 | eleq12d 2832 |
. . . . 5
β’ (π = π β ((π¦βπ) β ((π« π β© Fin) β {β
}) β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
147 | 141, 146 | imbi12d 345 |
. . . 4
β’ (π = π β ((π β β
β (π¦βπ) β ((π« π β© Fin) β {β
})) β (π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
})))) |
148 | 147 | cbvralvw 3228 |
. . 3
β’
(βπ β
π« (π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β {β
})) β
βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
149 | 140, 148 | sylib 217 |
. 2
β’ (π β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
150 | 29, 37, 45, 84, 98, 99, 138, 139, 149 | aomclem7 41416 |
1
β’ (π β βπ π We (π
1βπ΄)) |