Step | Hyp | Ref
| Expression |
1 | | coass 6222 |
. . . . 5
β’ ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€}))) = (π΄ β ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€})))) |
2 | | df1o2 8424 |
. . . . . . . . 9
β’
1o = {β
} |
3 | | pf1ind.cb |
. . . . . . . . . 10
β’ π΅ = (Baseβπ
) |
4 | 3 | fvexi 6861 |
. . . . . . . . 9
β’ π΅ β V |
5 | | 0ex 5269 |
. . . . . . . . 9
β’ β
β V |
6 | | eqid 2737 |
. . . . . . . . 9
β’ (π β (π΅ βm 1o) β¦
(πββ
)) = (π β (π΅ βm 1o) β¦
(πββ
)) |
7 | 2, 4, 5, 6 | mapsncnv 8838 |
. . . . . . . 8
β’ β‘(π β (π΅ βm 1o) β¦
(πββ
)) = (π€ β π΅ β¦ (1o Γ {π€})) |
8 | 7 | coeq2i 5821 |
. . . . . . 7
β’ ((π β (π΅ βm 1o) β¦
(πββ
)) β
β‘(π β (π΅ βm 1o) β¦
(πββ
))) =
((π β (π΅ βm
1o) β¦ (πββ
)) β (π€ β π΅ β¦ (1o Γ {π€}))) |
9 | 2, 4, 5, 6 | mapsnf1o2 8839 |
. . . . . . . 8
β’ (π β (π΅ βm 1o) β¦
(πββ
)):(π΅ βm
1o)β1-1-ontoβπ΅ |
10 | | f1ococnv2 6816 |
. . . . . . . 8
β’ ((π β (π΅ βm 1o) β¦
(πββ
)):(π΅ βm
1o)β1-1-ontoβπ΅ β ((π β (π΅ βm 1o) β¦
(πββ
)) β
β‘(π β (π΅ βm 1o) β¦
(πββ
))) = ( I
βΎ π΅)) |
11 | 9, 10 | mp1i 13 |
. . . . . . 7
β’ (π β ((π β (π΅ βm 1o) β¦
(πββ
)) β
β‘(π β (π΅ βm 1o) β¦
(πββ
))) = ( I
βΎ π΅)) |
12 | 8, 11 | eqtr3id 2791 |
. . . . . 6
β’ (π β ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€}))) = ( I βΎ π΅)) |
13 | 12 | coeq2d 5823 |
. . . . 5
β’ (π β (π΄ β ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€})))) = (π΄ β ( I βΎ π΅))) |
14 | 1, 13 | eqtrid 2789 |
. . . 4
β’ (π β ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€}))) = (π΄ β ( I βΎ π΅))) |
15 | | pf1ind.a |
. . . . 5
β’ (π β π΄ β π) |
16 | | pf1ind.cq |
. . . . . 6
β’ π = ran
(eval1βπ
) |
17 | 16, 3 | pf1f 21732 |
. . . . 5
β’ (π΄ β π β π΄:π΅βΆπ΅) |
18 | | fcoi1 6721 |
. . . . 5
β’ (π΄:π΅βΆπ΅ β (π΄ β ( I βΎ π΅)) = π΄) |
19 | 15, 17, 18 | 3syl 18 |
. . . 4
β’ (π β (π΄ β ( I βΎ π΅)) = π΄) |
20 | 14, 19 | eqtrd 2777 |
. . 3
β’ (π β ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€}))) = π΄) |
21 | | pf1ind.cp |
. . . 4
β’ + =
(+gβπ
) |
22 | | pf1ind.ct |
. . . 4
β’ Β· =
(.rβπ
) |
23 | | eqid 2737 |
. . . . . 6
β’
(1o eval π
) = (1o eval π
) |
24 | 23, 3 | evlval 21521 |
. . . . 5
β’
(1o eval π
) = ((1o evalSub π
)βπ΅) |
25 | 24 | rneqi 5897 |
. . . 4
β’ ran
(1o eval π
) =
ran ((1o evalSub π
)βπ΅) |
26 | | an4 655 |
. . . . . 6
β’ (((π β ran (1o eval
π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ (π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) β ((π β ran (1o eval π
) β§ π β ran (1o eval π
)) β§ ((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}))) |
27 | | eqid 2737 |
. . . . . . . . . . . 12
β’ ran
(1o eval π
) =
ran (1o eval π
) |
28 | 16, 3, 27 | mpfpf1 21733 |
. . . . . . . . . . 11
β’ (π β ran (1o eval
π
) β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β π) |
29 | 16, 3, 27 | mpfpf1 21733 |
. . . . . . . . . . 11
β’ (π β ran (1o eval
π
) β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β π) |
30 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
31 | | pf1ind.wc |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π β π)) |
32 | 30, 31 | elab 3635 |
. . . . . . . . . . . . . . . 16
β’ (π β {π₯ β£ π} β π) |
33 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β {π₯ β£ π} β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
34 | 32, 33 | bitr3id 285 |
. . . . . . . . . . . . . . 15
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
35 | 34 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((π β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π))) |
36 | 35 | anbi1d 631 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((π β§ π) β§ π) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π))) |
37 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (π βf + π) β V |
38 | | pf1ind.we |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π βf + π) β (π β π)) |
39 | 37, 38 | elab 3635 |
. . . . . . . . . . . . . 14
β’ ((π βf + π) β {π₯ β£ π} β π) |
40 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π βf + π) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π)) |
41 | 40 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((π βf + π) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) β {π₯ β£ π})) |
42 | 39, 41 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) β {π₯ β£ π})) |
43 | 36, 42 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((((π β§ π) β§ π) β π) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) β {π₯ β£ π}))) |
44 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
45 | | pf1ind.wd |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π β π)) |
46 | 44, 45 | elab 3635 |
. . . . . . . . . . . . . . . 16
β’ (π β {π₯ β£ π} β π) |
47 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β {π₯ β£ π} β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
48 | 46, 47 | bitr3id 285 |
. . . . . . . . . . . . . . 15
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
49 | 48 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}))) |
50 | 49 | anbi1d 631 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π))) |
51 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€}))))) |
52 | 51 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
53 | 50, 52 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + π) β {π₯ β£ π}) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π}))) |
54 | | pf1ind.ad |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) |
55 | 54 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π) β§ (π β π β§ π)) β (π β π)) |
56 | 55 | an4s 659 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β π) β§ (π β§ π)) β (π β π)) |
57 | 56 | expimpd 455 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (((π β§ π) β§ π) β π)) |
58 | 43, 53, 57 | vtocl2ga 3538 |
. . . . . . . . . . 11
β’ (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β π β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β π) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
59 | 28, 29, 58 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β ran (1o eval
π
) β§ π β ran (1o eval π
)) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
60 | 59 | expcomd 418 |
. . . . . . . . 9
β’ ((π β ran (1o eval
π
) β§ π β ran (1o eval π
)) β (π β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π}))) |
61 | 60 | impcom 409 |
. . . . . . . 8
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
62 | 25, 3 | mpff 21530 |
. . . . . . . . . . . 12
β’ (π β ran (1o eval
π
) β π:(π΅ βm
1o)βΆπ΅) |
63 | 62 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β π:(π΅ βm
1o)βΆπ΅) |
64 | 63 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β π Fn (π΅ βm
1o)) |
65 | 25, 3 | mpff 21530 |
. . . . . . . . . . . 12
β’ (π β ran (1o eval
π
) β π:(π΅ βm
1o)βΆπ΅) |
66 | 65 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β π:(π΅ βm
1o)βΆπ΅) |
67 | 66 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β π Fn (π΅ βm
1o)) |
68 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π€ β π΅ β¦ (1o Γ {π€})) = (π€ β π΅ β¦ (1o Γ {π€})) |
69 | 2, 4, 5, 68 | mapsnf1o3 8840 |
. . . . . . . . . . 11
β’ (π€ β π΅ β¦ (1o Γ {π€})):π΅β1-1-ontoβ(π΅ βm
1o) |
70 | | f1of 6789 |
. . . . . . . . . . 11
β’ ((π€ β π΅ β¦ (1o Γ {π€})):π΅β1-1-ontoβ(π΅ βm 1o) β
(π€ β π΅ β¦ (1o Γ {π€})):π΅βΆ(π΅ βm
1o)) |
71 | 69, 70 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (π€ β π΅ β¦ (1o Γ {π€})):π΅βΆ(π΅ βm
1o)) |
72 | | ovexd 7397 |
. . . . . . . . . 10
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (π΅ βm 1o) β
V) |
73 | 4 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β π΅ β V) |
74 | | inidm 4183 |
. . . . . . . . . 10
β’ ((π΅ βm
1o) β© (π΅
βm 1o)) = (π΅ βm
1o) |
75 | 64, 67, 71, 72, 72, 73, 74 | ofco 7645 |
. . . . . . . . 9
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€}))))) |
76 | 75 | eleq1d 2823 |
. . . . . . . 8
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf + (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
77 | 61, 76 | sylibrd 259 |
. . . . . . 7
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
78 | 77 | expimpd 455 |
. . . . . 6
β’ (π β (((π β ran (1o eval π
) β§ π β ran (1o eval π
)) β§ ((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
79 | 26, 78 | biimtrid 241 |
. . . . 5
β’ (π β (((π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ (π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
80 | 79 | imp 408 |
. . . 4
β’ ((π β§ ((π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ (π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}))) β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
81 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (π βf Β· π) β V |
82 | | pf1ind.wf |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π βf Β· π) β (π β π)) |
83 | 81, 82 | elab 3635 |
. . . . . . . . . . . . . 14
β’ ((π βf Β· π) β {π₯ β£ π} β π) |
84 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π βf Β· π) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π)) |
85 | 84 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((π βf Β· π) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) β {π₯ β£ π})) |
86 | 83, 85 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (π β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) β {π₯ β£ π})) |
87 | 36, 86 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((((π β§ π) β§ π) β π) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) β {π₯ β£ π}))) |
88 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€}))))) |
89 | 88 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
90 | 50, 89 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = (π β (π€ β π΅ β¦ (1o Γ {π€}))) β (((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ π) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· π) β {π₯ β£ π}) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π}))) |
91 | | pf1ind.mu |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) |
92 | 91 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π) β§ (π β π β§ π)) β (π β π)) |
93 | 92 | an4s 659 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β π) β§ (π β§ π)) β (π β π)) |
94 | 93 | expimpd 455 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (((π β§ π) β§ π) β π)) |
95 | 87, 90, 94 | vtocl2ga 3538 |
. . . . . . . . . . 11
β’ (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β π β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β π) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
96 | 28, 29, 95 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β ran (1o eval
π
) β§ π β ran (1o eval π
)) β ((((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ π) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
97 | 96 | expcomd 418 |
. . . . . . . . 9
β’ ((π β ran (1o eval
π
) β§ π β ran (1o eval π
)) β (π β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π}))) |
98 | 97 | impcom 409 |
. . . . . . . 8
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
99 | 64, 67, 71, 72, 72, 73, 74 | ofco 7645 |
. . . . . . . . 9
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€}))))) |
100 | 99 | eleq1d 2823 |
. . . . . . . 8
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π β (π€ β π΅ β¦ (1o Γ {π€}))) βf Β· (π β (π€ β π΅ β¦ (1o Γ {π€})))) β {π₯ β£ π})) |
101 | 98, 100 | sylibrd 259 |
. . . . . . 7
β’ ((π β§ (π β ran (1o eval π
) β§ π β ran (1o eval π
))) β (((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
102 | 101 | expimpd 455 |
. . . . . 6
β’ (π β (((π β ran (1o eval π
) β§ π β ran (1o eval π
)) β§ ((π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
103 | 26, 102 | biimtrid 241 |
. . . . 5
β’ (π β (((π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ (π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
104 | 103 | imp 408 |
. . . 4
β’ ((π β§ ((π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) β§ (π β ran (1o eval π
) β§ (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}))) β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
105 | | coeq1 5818 |
. . . . 5
β’ (π¦ = ((π΅ βm 1o) Γ
{π}) β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = (((π΅ βm 1o) Γ
{π}) β (π€ β π΅ β¦ (1o Γ {π€})))) |
106 | 105 | eleq1d 2823 |
. . . 4
β’ (π¦ = ((π΅ βm 1o) Γ
{π}) β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β (((π΅ βm 1o) Γ
{π}) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
107 | | coeq1 5818 |
. . . . 5
β’ (π¦ = (π β (π΅ βm 1o) β¦
(πβπ)) β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π β (π΅ βm 1o) β¦
(πβπ)) β (π€ β π΅ β¦ (1o Γ {π€})))) |
108 | 107 | eleq1d 2823 |
. . . 4
β’ (π¦ = (π β (π΅ βm 1o) β¦
(πβπ)) β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π β (π΅ βm 1o) β¦
(πβπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
109 | | coeq1 5818 |
. . . . 5
β’ (π¦ = π β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = (π β (π€ β π΅ β¦ (1o Γ {π€})))) |
110 | 109 | eleq1d 2823 |
. . . 4
β’ (π¦ = π β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
111 | | coeq1 5818 |
. . . . 5
β’ (π¦ = π β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = (π β (π€ β π΅ β¦ (1o Γ {π€})))) |
112 | 111 | eleq1d 2823 |
. . . 4
β’ (π¦ = π β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β (π β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
113 | | coeq1 5818 |
. . . . 5
β’ (π¦ = (π βf + π) β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€})))) |
114 | 113 | eleq1d 2823 |
. . . 4
β’ (π¦ = (π βf + π) β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π βf + π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
115 | | coeq1 5818 |
. . . . 5
β’ (π¦ = (π βf Β· π) β (π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€})))) |
116 | 115 | eleq1d 2823 |
. . . 4
β’ (π¦ = (π βf Β· π) β ((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π βf Β· π) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
117 | | coeq1 5818 |
. . . . 5
β’ (π¦ = (π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€})))) |
118 | 117 | eleq1d 2823 |
. . . 4
β’ (π¦ = (π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
((π¦ β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
119 | 16 | pf1rcl 21731 |
. . . . . . . . 9
β’ (π΄ β π β π
β CRing) |
120 | 15, 119 | syl 17 |
. . . . . . . 8
β’ (π β π
β CRing) |
121 | 120 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΅) β π
β CRing) |
122 | | 1on 8429 |
. . . . . . . . . . . 12
β’
1o β On |
123 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(1o mPoly π
) = (1o mPoly π
) |
124 | 123 | mplassa 21443 |
. . . . . . . . . . . 12
β’
((1o β On β§ π
β CRing) β (1o mPoly
π
) β
AssAlg) |
125 | 122, 120,
124 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (1o mPoly π
) β
AssAlg) |
126 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Poly1βπ
) = (Poly1βπ
) |
127 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(algScβ(Poly1βπ
)) =
(algScβ(Poly1βπ
)) |
128 | 126, 127 | ply1ascl 21645 |
. . . . . . . . . . . 12
β’
(algScβ(Poly1βπ
)) = (algScβ(1o mPoly π
)) |
129 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Scalarβ(1o mPoly π
)) = (Scalarβ(1o mPoly
π
)) |
130 | 128, 129 | asclrhm 21309 |
. . . . . . . . . . 11
β’
((1o mPoly π
) β AssAlg β
(algScβ(Poly1βπ
)) β ((Scalarβ(1o
mPoly π
)) RingHom
(1o mPoly π
))) |
131 | 125, 130 | syl 17 |
. . . . . . . . . 10
β’ (π β
(algScβ(Poly1βπ
)) β ((Scalarβ(1o
mPoly π
)) RingHom
(1o mPoly π
))) |
132 | 122 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1o β
On) |
133 | 123, 132,
120 | mplsca 21433 |
. . . . . . . . . . 11
β’ (π β π
= (Scalarβ(1o mPoly π
))) |
134 | 133 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β (π
RingHom (1o mPoly π
)) =
((Scalarβ(1o mPoly π
)) RingHom (1o mPoly π
))) |
135 | 131, 134 | eleqtrrd 2841 |
. . . . . . . . 9
β’ (π β
(algScβ(Poly1βπ
)) β (π
RingHom (1o mPoly π
))) |
136 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβ(1o mPoly π
)) = (Baseβ(1o mPoly π
)) |
137 | 3, 136 | rhmf 20167 |
. . . . . . . . 9
β’
((algScβ(Poly1βπ
)) β (π
RingHom (1o mPoly π
)) β
(algScβ(Poly1βπ
)):π΅βΆ(Baseβ(1o mPoly
π
))) |
138 | 135, 137 | syl 17 |
. . . . . . . 8
β’ (π β
(algScβ(Poly1βπ
)):π΅βΆ(Baseβ(1o mPoly
π
))) |
139 | 138 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β π΅) β
((algScβ(Poly1βπ
))βπ) β (Baseβ(1o mPoly
π
))) |
140 | | eqid 2737 |
. . . . . . . 8
β’
(eval1βπ
) = (eval1βπ
) |
141 | 140, 23, 3, 123, 136 | evl1val 21711 |
. . . . . . 7
β’ ((π
β CRing β§
((algScβ(Poly1βπ
))βπ) β (Baseβ(1o mPoly
π
))) β
((eval1βπ
)β((algScβ(Poly1βπ
))βπ)) = (((1o eval π
)β((algScβ(Poly1βπ
))βπ)) β (π€ β π΅ β¦ (1o Γ {π€})))) |
142 | 121, 139,
141 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π΅) β ((eval1βπ
)β((algScβ(Poly1βπ
))βπ)) = (((1o eval π
)β((algScβ(Poly1βπ
))βπ)) β (π€ β π΅ β¦ (1o Γ {π€})))) |
143 | 140, 126,
3, 127 | evl1sca 21716 |
. . . . . . 7
β’ ((π
β CRing β§ π β π΅) β ((eval1βπ
)β((algScβ(Poly1βπ
))βπ)) = (π΅ Γ {π})) |
144 | 120, 143 | sylan 581 |
. . . . . 6
β’ ((π β§ π β π΅) β ((eval1βπ
)β((algScβ(Poly1βπ
))βπ)) = (π΅ Γ {π})) |
145 | 3 | ressid 17132 |
. . . . . . . . . . . . . 14
β’ (π
β CRing β (π
βΎs π΅) = π
) |
146 | 121, 145 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π
βΎs π΅) = π
) |
147 | 146 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (1o mPoly (π
βΎs π΅)) = (1o mPoly π
)) |
148 | 147 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (algScβ(1o mPoly
(π
βΎs
π΅))) =
(algScβ(1o mPoly π
))) |
149 | 148, 128 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (algScβ(1o mPoly
(π
βΎs
π΅))) =
(algScβ(Poly1βπ
))) |
150 | 149 | fveq1d 6849 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β ((algScβ(1o mPoly
(π
βΎs
π΅)))βπ) =
((algScβ(Poly1βπ
))βπ)) |
151 | 150 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π β π΅) β ((1o eval π
)β((algScβ(1o mPoly
(π
βΎs
π΅)))βπ)) = ((1o eval π
)β((algScβ(Poly1βπ
))βπ))) |
152 | | eqid 2737 |
. . . . . . . . 9
β’
(1o mPoly (π
βΎs π΅)) = (1o mPoly (π
βΎs π΅)) |
153 | | eqid 2737 |
. . . . . . . . 9
β’ (π
βΎs π΅) = (π
βΎs π΅) |
154 | | eqid 2737 |
. . . . . . . . 9
β’
(algScβ(1o mPoly (π
βΎs π΅))) = (algScβ(1o mPoly
(π
βΎs
π΅))) |
155 | 122 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β 1o β
On) |
156 | | crngring 19983 |
. . . . . . . . . . 11
β’ (π
β CRing β π
β Ring) |
157 | 3 | subrgid 20240 |
. . . . . . . . . . 11
β’ (π
β Ring β π΅ β (SubRingβπ
)) |
158 | 120, 156,
157 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π΅ β (SubRingβπ
)) |
159 | 158 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π΅ β (SubRingβπ
)) |
160 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β π΅) |
161 | 24, 152, 153, 3, 154, 155, 121, 159, 160 | evlssca 21515 |
. . . . . . . 8
β’ ((π β§ π β π΅) β ((1o eval π
)β((algScβ(1o mPoly
(π
βΎs
π΅)))βπ)) = ((π΅ βm 1o) Γ
{π})) |
162 | 151, 161 | eqtr3d 2779 |
. . . . . . 7
β’ ((π β§ π β π΅) β ((1o eval π
)β((algScβ(Poly1βπ
))βπ)) = ((π΅ βm 1o) Γ {π})) |
163 | 162 | coeq1d 5822 |
. . . . . 6
β’ ((π β§ π β π΅) β (((1o eval π
)β((algScβ(Poly1βπ
))βπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) = (((π΅ βm 1o) Γ {π}) β (π€ β π΅ β¦ (1o Γ {π€})))) |
164 | 142, 144,
163 | 3eqtr3d 2785 |
. . . . 5
β’ ((π β§ π β π΅) β (π΅ Γ {π}) = (((π΅ βm 1o) Γ
{π}) β (π€ β π΅ β¦ (1o Γ {π€})))) |
165 | | pf1ind.co |
. . . . . . . 8
β’ ((π β§ π β π΅) β π) |
166 | | vsnex 5391 |
. . . . . . . . . 10
β’ {π} β V |
167 | 4, 166 | xpex 7692 |
. . . . . . . . 9
β’ (π΅ Γ {π}) β V |
168 | | pf1ind.wa |
. . . . . . . . 9
β’ (π₯ = (π΅ Γ {π}) β (π β π)) |
169 | 167, 168 | elab 3635 |
. . . . . . . 8
β’ ((π΅ Γ {π}) β {π₯ β£ π} β π) |
170 | 165, 169 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π΅ Γ {π}) β {π₯ β£ π}) |
171 | 170 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β π΅ (π΅ Γ {π}) β {π₯ β£ π}) |
172 | | sneq 4601 |
. . . . . . . . 9
β’ (π = π β {π} = {π}) |
173 | 172 | xpeq2d 5668 |
. . . . . . . 8
β’ (π = π β (π΅ Γ {π}) = (π΅ Γ {π})) |
174 | 173 | eleq1d 2823 |
. . . . . . 7
β’ (π = π β ((π΅ Γ {π}) β {π₯ β£ π} β (π΅ Γ {π}) β {π₯ β£ π})) |
175 | 174 | rspccva 3583 |
. . . . . 6
β’
((βπ β
π΅ (π΅ Γ {π}) β {π₯ β£ π} β§ π β π΅) β (π΅ Γ {π}) β {π₯ β£ π}) |
176 | 171, 175 | sylan 581 |
. . . . 5
β’ ((π β§ π β π΅) β (π΅ Γ {π}) β {π₯ β£ π}) |
177 | 164, 176 | eqeltrrd 2839 |
. . . 4
β’ ((π β§ π β π΅) β (((π΅ βm 1o) Γ
{π}) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
178 | | pf1ind.pr |
. . . . . . . 8
β’ (π β π) |
179 | | resiexg 7856 |
. . . . . . . . . 10
β’ (π΅ β V β ( I βΎ
π΅) β
V) |
180 | 4, 179 | ax-mp 5 |
. . . . . . . . 9
β’ ( I
βΎ π΅) β
V |
181 | | pf1ind.wb |
. . . . . . . . 9
β’ (π₯ = ( I βΎ π΅) β (π β π)) |
182 | 180, 181 | elab 3635 |
. . . . . . . 8
β’ (( I
βΎ π΅) β {π₯ β£ π} β π) |
183 | 178, 182 | sylibr 233 |
. . . . . . 7
β’ (π β ( I βΎ π΅) β {π₯ β£ π}) |
184 | 12, 183 | eqeltrd 2838 |
. . . . . 6
β’ (π β ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
185 | | el1o 8446 |
. . . . . . . . . 10
β’ (π β 1o β
π =
β
) |
186 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = β
β (πβπ) = (πββ
)) |
187 | 185, 186 | sylbi 216 |
. . . . . . . . 9
β’ (π β 1o β
(πβπ) = (πββ
)) |
188 | 187 | mpteq2dv 5212 |
. . . . . . . 8
β’ (π β 1o β
(π β (π΅ βm
1o) β¦ (πβπ)) = (π β (π΅ βm 1o) β¦
(πββ
))) |
189 | 188 | coeq1d 5822 |
. . . . . . 7
β’ (π β 1o β
((π β (π΅ βm
1o) β¦ (πβπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) = ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€})))) |
190 | 189 | eleq1d 2823 |
. . . . . 6
β’ (π β 1o β
(((π β (π΅ βm
1o) β¦ (πβπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π} β ((π β (π΅ βm 1o) β¦
(πββ
)) β
(π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
191 | 184, 190 | syl5ibrcom 247 |
. . . . 5
β’ (π β (π β 1o β ((π β (π΅ βm 1o) β¦
(πβπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π})) |
192 | 191 | imp 408 |
. . . 4
β’ ((π β§ π β 1o) β ((π β (π΅ βm 1o) β¦
(πβπ)) β (π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
193 | 16, 3, 27 | pf1mpf 21734 |
. . . . 5
β’ (π΄ β π β (π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
ran (1o eval π
)) |
194 | 15, 193 | syl 17 |
. . . 4
β’ (π β (π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
ran (1o eval π
)) |
195 | 3, 21, 22, 25, 80, 104, 106, 108, 110, 112, 114, 116, 118, 177, 192, 194 | mpfind 21533 |
. . 3
β’ (π β ((π΄ β (π β (π΅ βm 1o) β¦
(πββ
))) β
(π€ β π΅ β¦ (1o Γ {π€}))) β {π₯ β£ π}) |
196 | 20, 195 | eqeltrrd 2839 |
. 2
β’ (π β π΄ β {π₯ β£ π}) |
197 | | pf1ind.wg |
. . . 4
β’ (π₯ = π΄ β (π β π)) |
198 | 197 | elabg 3633 |
. . 3
β’ (π΄ β π β (π΄ β {π₯ β£ π} β π)) |
199 | 15, 198 | syl 17 |
. 2
β’ (π β (π΄ β {π₯ β£ π} β π)) |
200 | 196, 199 | mpbid 231 |
1
β’ (π β π) |