Step | Hyp | Ref
| Expression |
1 | | tsmsfbas.a |
. 2
β’ (π β π΄ β π) |
2 | | elex 3466 |
. 2
β’ (π΄ β π β π΄ β V) |
3 | | tsmsfbas.l |
. . 3
β’ πΏ = ran πΉ |
4 | | ssrab2 4042 |
. . . . . . 7
β’ {π¦ β π β£ π§ β π¦} β π |
5 | | tsmsfbas.s |
. . . . . . . . . 10
β’ π = (π« π΄ β© Fin) |
6 | | pwexg 5338 |
. . . . . . . . . . 11
β’ (π΄ β V β π« π΄ β V) |
7 | | inex1g 5281 |
. . . . . . . . . . 11
β’
(π« π΄ β
V β (π« π΄ β©
Fin) β V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β V β (π«
π΄ β© Fin) β
V) |
9 | 5, 8 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π΄ β V β π β V) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β V β§ π§ β π) β π β V) |
11 | | elpw2g 5306 |
. . . . . . . 8
β’ (π β V β ({π¦ β π β£ π§ β π¦} β π« π β {π¦ β π β£ π§ β π¦} β π)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ ((π΄ β V β§ π§ β π) β ({π¦ β π β£ π§ β π¦} β π« π β {π¦ β π β£ π§ β π¦} β π)) |
13 | 4, 12 | mpbiri 258 |
. . . . . 6
β’ ((π΄ β V β§ π§ β π) β {π¦ β π β£ π§ β π¦} β π« π) |
14 | | tsmsfbas.f |
. . . . . 6
β’ πΉ = (π§ β π β¦ {π¦ β π β£ π§ β π¦}) |
15 | 13, 14 | fmptd 7067 |
. . . . 5
β’ (π΄ β V β πΉ:πβΆπ« π) |
16 | 15 | frnd 6681 |
. . . 4
β’ (π΄ β V β ran πΉ β π« π) |
17 | | 0ss 4361 |
. . . . . . . . . 10
β’ β
β π΄ |
18 | | 0fin 9122 |
. . . . . . . . . 10
β’ β
β Fin |
19 | | elfpw 9305 |
. . . . . . . . . 10
β’ (β
β (π« π΄ β©
Fin) β (β
β π΄ β§ β
β Fin)) |
20 | 17, 18, 19 | mpbir2an 710 |
. . . . . . . . 9
β’ β
β (π« π΄ β©
Fin) |
21 | 20, 5 | eleqtrri 2837 |
. . . . . . . 8
β’ β
β π |
22 | | 0ss 4361 |
. . . . . . . . 9
β’ β
β π¦ |
23 | 22 | rgenw 3069 |
. . . . . . . 8
β’
βπ¦ β
π β
β π¦ |
24 | | rabid2 3439 |
. . . . . . . . . 10
β’ (π = {π¦ β π β£ π§ β π¦} β βπ¦ β π π§ β π¦) |
25 | | sseq1 3974 |
. . . . . . . . . . 11
β’ (π§ = β
β (π§ β π¦ β β
β π¦)) |
26 | 25 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π§ = β
β (βπ¦ β π π§ β π¦ β βπ¦ β π β
β π¦)) |
27 | 24, 26 | bitrid 283 |
. . . . . . . . 9
β’ (π§ = β
β (π = {π¦ β π β£ π§ β π¦} β βπ¦ β π β
β π¦)) |
28 | 27 | rspcev 3584 |
. . . . . . . 8
β’ ((β
β π β§
βπ¦ β π β
β π¦) β βπ§ β π π = {π¦ β π β£ π§ β π¦}) |
29 | 21, 23, 28 | mp2an 691 |
. . . . . . 7
β’
βπ§ β
π π = {π¦ β π β£ π§ β π¦} |
30 | 14 | elrnmpt 5916 |
. . . . . . . 8
β’ (π β V β (π β ran πΉ β βπ§ β π π = {π¦ β π β£ π§ β π¦})) |
31 | 9, 30 | syl 17 |
. . . . . . 7
β’ (π΄ β V β (π β ran πΉ β βπ§ β π π = {π¦ β π β£ π§ β π¦})) |
32 | 29, 31 | mpbiri 258 |
. . . . . 6
β’ (π΄ β V β π β ran πΉ) |
33 | 32 | ne0d 4300 |
. . . . 5
β’ (π΄ β V β ran πΉ β β
) |
34 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π΄ β V β§ π§ β π) β π§ β π) |
35 | | ssid 3971 |
. . . . . . . . . . . 12
β’ π§ β π§ |
36 | | sseq2 3975 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (π§ β π¦ β π§ β π§)) |
37 | 36 | rspcev 3584 |
. . . . . . . . . . . 12
β’ ((π§ β π β§ π§ β π§) β βπ¦ β π π§ β π¦) |
38 | 34, 35, 37 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ π§ β π) β βπ¦ β π π§ β π¦) |
39 | | rabn0 4350 |
. . . . . . . . . . 11
β’ ({π¦ β π β£ π§ β π¦} β β
β βπ¦ β π π§ β π¦) |
40 | 38, 39 | sylibr 233 |
. . . . . . . . . 10
β’ ((π΄ β V β§ π§ β π) β {π¦ β π β£ π§ β π¦} β β
) |
41 | 40 | necomd 3000 |
. . . . . . . . 9
β’ ((π΄ β V β§ π§ β π) β β
β {π¦ β π β£ π§ β π¦}) |
42 | 41 | neneqd 2949 |
. . . . . . . 8
β’ ((π΄ β V β§ π§ β π) β Β¬ β
= {π¦ β π β£ π§ β π¦}) |
43 | 42 | nrexdv 3147 |
. . . . . . 7
β’ (π΄ β V β Β¬
βπ§ β π β
= {π¦ β π β£ π§ β π¦}) |
44 | | 0ex 5269 |
. . . . . . . 8
β’ β
β V |
45 | 14 | elrnmpt 5916 |
. . . . . . . 8
β’ (β
β V β (β
β ran πΉ β βπ§ β π β
= {π¦ β π β£ π§ β π¦})) |
46 | 44, 45 | ax-mp 5 |
. . . . . . 7
β’ (β
β ran πΉ β
βπ§ β π β
= {π¦ β π β£ π§ β π¦}) |
47 | 43, 46 | sylnibr 329 |
. . . . . 6
β’ (π΄ β V β Β¬ β
β ran πΉ) |
48 | | df-nel 3051 |
. . . . . 6
β’ (β
β ran πΉ β Β¬
β
β ran πΉ) |
49 | 47, 48 | sylibr 233 |
. . . . 5
β’ (π΄ β V β β
β
ran πΉ) |
50 | | elfpw 9305 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β (π« π΄ β© Fin) β (π’ β π΄ β§ π’ β Fin)) |
51 | 50 | simplbi 499 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β (π« π΄ β© Fin) β π’ β π΄) |
52 | 51, 5 | eleq2s 2856 |
. . . . . . . . . . . . . . . 16
β’ (π’ β π β π’ β π΄) |
53 | | elfpw 9305 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β (π« π΄ β© Fin) β (π£ β π΄ β§ π£ β Fin)) |
54 | 53 | simplbi 499 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β (π« π΄ β© Fin) β π£ β π΄) |
55 | 54, 5 | eleq2s 2856 |
. . . . . . . . . . . . . . . 16
β’ (π£ β π β π£ β π΄) |
56 | 52, 55 | anim12i 614 |
. . . . . . . . . . . . . . 15
β’ ((π’ β π β§ π£ β π) β (π’ β π΄ β§ π£ β π΄)) |
57 | | unss 4149 |
. . . . . . . . . . . . . . 15
β’ ((π’ β π΄ β§ π£ β π΄) β (π’ βͺ π£) β π΄) |
58 | 56, 57 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π£ β π) β (π’ βͺ π£) β π΄) |
59 | | elinel2 4161 |
. . . . . . . . . . . . . . . 16
β’ (π’ β (π« π΄ β© Fin) β π’ β Fin) |
60 | 59, 5 | eleq2s 2856 |
. . . . . . . . . . . . . . 15
β’ (π’ β π β π’ β Fin) |
61 | | elinel2 4161 |
. . . . . . . . . . . . . . . 16
β’ (π£ β (π« π΄ β© Fin) β π£ β Fin) |
62 | 61, 5 | eleq2s 2856 |
. . . . . . . . . . . . . . 15
β’ (π£ β π β π£ β Fin) |
63 | | unfi 9123 |
. . . . . . . . . . . . . . 15
β’ ((π’ β Fin β§ π£ β Fin) β (π’ βͺ π£) β Fin) |
64 | 60, 62, 63 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π£ β π) β (π’ βͺ π£) β Fin) |
65 | | elfpw 9305 |
. . . . . . . . . . . . . 14
β’ ((π’ βͺ π£) β (π« π΄ β© Fin) β ((π’ βͺ π£) β π΄ β§ (π’ βͺ π£) β Fin)) |
66 | 58, 64, 65 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π£ β π) β (π’ βͺ π£) β (π« π΄ β© Fin)) |
67 | 66 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β (π’ βͺ π£) β (π« π΄ β© Fin)) |
68 | 67, 5 | eleqtrrdi 2849 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β (π’ βͺ π£) β π) |
69 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ (π’ βͺ π£) β π¦}) |
70 | | sseq1 3974 |
. . . . . . . . . . . . 13
β’ (π = (π’ βͺ π£) β (π β π¦ β (π’ βͺ π£) β π¦)) |
71 | 70 | rabbidv 3418 |
. . . . . . . . . . . 12
β’ (π = (π’ βͺ π£) β {π¦ β π β£ π β π¦} = {π¦ β π β£ (π’ βͺ π£) β π¦}) |
72 | 71 | rspceeqv 3600 |
. . . . . . . . . . 11
β’ (((π’ βͺ π£) β π β§ {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ (π’ βͺ π£) β π¦}) β βπ β π {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ π β π¦}) |
73 | 68, 69, 72 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β βπ β π {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ π β π¦}) |
74 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β π β V) |
75 | | rabexg 5293 |
. . . . . . . . . . . 12
β’ (π β V β {π¦ β π β£ (π’ βͺ π£) β π¦} β V) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β {π¦ β π β£ (π’ βͺ π£) β π¦} β V) |
77 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β (π§ β π¦ β π β π¦)) |
78 | 77 | rabbidv 3418 |
. . . . . . . . . . . . . 14
β’ (π§ = π β {π¦ β π β£ π§ β π¦} = {π¦ β π β£ π β π¦}) |
79 | 78 | cbvmptv 5223 |
. . . . . . . . . . . . 13
β’ (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = (π β π β¦ {π¦ β π β£ π β π¦}) |
80 | 14, 79 | eqtri 2765 |
. . . . . . . . . . . 12
β’ πΉ = (π β π β¦ {π¦ β π β£ π β π¦}) |
81 | 80 | elrnmpt 5916 |
. . . . . . . . . . 11
β’ ({π¦ β π β£ (π’ βͺ π£) β π¦} β V β ({π¦ β π β£ (π’ βͺ π£) β π¦} β ran πΉ β βπ β π {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ π β π¦})) |
82 | 76, 81 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β ({π¦ β π β£ (π’ βͺ π£) β π¦} β ran πΉ β βπ β π {π¦ β π β£ (π’ βͺ π£) β π¦} = {π¦ β π β£ π β π¦})) |
83 | 73, 82 | mpbird 257 |
. . . . . . . . 9
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β {π¦ β π β£ (π’ βͺ π£) β π¦} β ran πΉ) |
84 | | pwidg 4585 |
. . . . . . . . . 10
β’ ({π¦ β π β£ (π’ βͺ π£) β π¦} β V β {π¦ β π β£ (π’ βͺ π£) β π¦} β π« {π¦ β π β£ (π’ βͺ π£) β π¦}) |
85 | 76, 84 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β {π¦ β π β£ (π’ βͺ π£) β π¦} β π« {π¦ β π β£ (π’ βͺ π£) β π¦}) |
86 | | inelcm 4429 |
. . . . . . . . 9
β’ (({π¦ β π β£ (π’ βͺ π£) β π¦} β ran πΉ β§ {π¦ β π β£ (π’ βͺ π£) β π¦} β π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
) |
87 | 83, 85, 86 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β V β§ (π’ β π β§ π£ β π)) β (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
) |
88 | 87 | ralrimivva 3198 |
. . . . . . 7
β’ (π΄ β V β βπ’ β π βπ£ β π (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
) |
89 | | rabexg 5293 |
. . . . . . . . . 10
β’ (π β V β {π¦ β π β£ π’ β π¦} β V) |
90 | 9, 89 | syl 17 |
. . . . . . . . 9
β’ (π΄ β V β {π¦ β π β£ π’ β π¦} β V) |
91 | 90 | ralrimivw 3148 |
. . . . . . . 8
β’ (π΄ β V β βπ’ β π {π¦ β π β£ π’ β π¦} β V) |
92 | | sseq1 3974 |
. . . . . . . . . . . 12
β’ (π§ = π’ β (π§ β π¦ β π’ β π¦)) |
93 | 92 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π§ = π’ β {π¦ β π β£ π§ β π¦} = {π¦ β π β£ π’ β π¦}) |
94 | 93 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = (π’ β π β¦ {π¦ β π β£ π’ β π¦}) |
95 | 14, 94 | eqtri 2765 |
. . . . . . . . 9
β’ πΉ = (π’ β π β¦ {π¦ β π β£ π’ β π¦}) |
96 | | ineq1 4170 |
. . . . . . . . . . . . . 14
β’ (π = {π¦ β π β£ π’ β π¦} β (π β© {π¦ β π β£ π£ β π¦}) = ({π¦ β π β£ π’ β π¦} β© {π¦ β π β£ π£ β π¦})) |
97 | | inrab 4271 |
. . . . . . . . . . . . . . 15
β’ ({π¦ β π β£ π’ β π¦} β© {π¦ β π β£ π£ β π¦}) = {π¦ β π β£ (π’ β π¦ β§ π£ β π¦)} |
98 | | unss 4149 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β π¦ β§ π£ β π¦) β (π’ βͺ π£) β π¦) |
99 | 98 | rabbii 3416 |
. . . . . . . . . . . . . . 15
β’ {π¦ β π β£ (π’ β π¦ β§ π£ β π¦)} = {π¦ β π β£ (π’ βͺ π£) β π¦} |
100 | 97, 99 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ ({π¦ β π β£ π’ β π¦} β© {π¦ β π β£ π£ β π¦}) = {π¦ β π β£ (π’ βͺ π£) β π¦} |
101 | 96, 100 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = {π¦ β π β£ π’ β π¦} β (π β© {π¦ β π β£ π£ β π¦}) = {π¦ β π β£ (π’ βͺ π£) β π¦}) |
102 | 101 | pweqd 4582 |
. . . . . . . . . . . 12
β’ (π = {π¦ β π β£ π’ β π¦} β π« (π β© {π¦ β π β£ π£ β π¦}) = π« {π¦ β π β£ (π’ βͺ π£) β π¦}) |
103 | 102 | ineq2d 4177 |
. . . . . . . . . . 11
β’ (π = {π¦ β π β£ π’ β π¦} β (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) = (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦})) |
104 | 103 | neeq1d 3004 |
. . . . . . . . . 10
β’ (π = {π¦ β π β£ π’ β π¦} β ((ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
β (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
)) |
105 | 104 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = {π¦ β π β£ π’ β π¦} β (βπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
β βπ£ β π (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
)) |
106 | 95, 105 | ralrnmptw 7049 |
. . . . . . . 8
β’
(βπ’ β
π {π¦ β π β£ π’ β π¦} β V β (βπ β ran πΉβπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
β βπ’ β π βπ£ β π (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
)) |
107 | 91, 106 | syl 17 |
. . . . . . 7
β’ (π΄ β V β (βπ β ran πΉβπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
β βπ’ β π βπ£ β π (ran πΉ β© π« {π¦ β π β£ (π’ βͺ π£) β π¦}) β β
)) |
108 | 88, 107 | mpbird 257 |
. . . . . 6
β’ (π΄ β V β βπ β ran πΉβπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
) |
109 | | rabexg 5293 |
. . . . . . . . . 10
β’ (π β V β {π¦ β π β£ π£ β π¦} β V) |
110 | 9, 109 | syl 17 |
. . . . . . . . 9
β’ (π΄ β V β {π¦ β π β£ π£ β π¦} β V) |
111 | 110 | ralrimivw 3148 |
. . . . . . . 8
β’ (π΄ β V β βπ£ β π {π¦ β π β£ π£ β π¦} β V) |
112 | | sseq1 3974 |
. . . . . . . . . . . 12
β’ (π§ = π£ β (π§ β π¦ β π£ β π¦)) |
113 | 112 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π§ = π£ β {π¦ β π β£ π§ β π¦} = {π¦ β π β£ π£ β π¦}) |
114 | 113 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π§ β π β¦ {π¦ β π β£ π§ β π¦}) = (π£ β π β¦ {π¦ β π β£ π£ β π¦}) |
115 | 14, 114 | eqtri 2765 |
. . . . . . . . 9
β’ πΉ = (π£ β π β¦ {π¦ β π β£ π£ β π¦}) |
116 | | ineq2 4171 |
. . . . . . . . . . . 12
β’ (π = {π¦ β π β£ π£ β π¦} β (π β© π) = (π β© {π¦ β π β£ π£ β π¦})) |
117 | 116 | pweqd 4582 |
. . . . . . . . . . 11
β’ (π = {π¦ β π β£ π£ β π¦} β π« (π β© π) = π« (π β© {π¦ β π β£ π£ β π¦})) |
118 | 117 | ineq2d 4177 |
. . . . . . . . . 10
β’ (π = {π¦ β π β£ π£ β π¦} β (ran πΉ β© π« (π β© π)) = (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦}))) |
119 | 118 | neeq1d 3004 |
. . . . . . . . 9
β’ (π = {π¦ β π β£ π£ β π¦} β ((ran πΉ β© π« (π β© π)) β β
β (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
)) |
120 | 115, 119 | ralrnmptw 7049 |
. . . . . . . 8
β’
(βπ£ β
π {π¦ β π β£ π£ β π¦} β V β (βπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
β βπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
)) |
121 | 111, 120 | syl 17 |
. . . . . . 7
β’ (π΄ β V β (βπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
β βπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
)) |
122 | 121 | ralbidv 3175 |
. . . . . 6
β’ (π΄ β V β (βπ β ran πΉβπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
β βπ β ran πΉβπ£ β π (ran πΉ β© π« (π β© {π¦ β π β£ π£ β π¦})) β β
)) |
123 | 108, 122 | mpbird 257 |
. . . . 5
β’ (π΄ β V β βπ β ran πΉβπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
) |
124 | 33, 49, 123 | 3jca 1129 |
. . . 4
β’ (π΄ β V β (ran πΉ β β
β§ β
β ran πΉ β§
βπ β ran πΉβπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
)) |
125 | | isfbas 23196 |
. . . . 5
β’ (π β V β (ran πΉ β (fBasβπ) β (ran πΉ β π« π β§ (ran πΉ β β
β§ β
β ran
πΉ β§ βπ β ran πΉβπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
)))) |
126 | 9, 125 | syl 17 |
. . . 4
β’ (π΄ β V β (ran πΉ β (fBasβπ) β (ran πΉ β π« π β§ (ran πΉ β β
β§ β
β ran
πΉ β§ βπ β ran πΉβπ β ran πΉ(ran πΉ β© π« (π β© π)) β β
)))) |
127 | 16, 124, 126 | mpbir2and 712 |
. . 3
β’ (π΄ β V β ran πΉ β (fBasβπ)) |
128 | 3, 127 | eqeltrid 2842 |
. 2
β’ (π΄ β V β πΏ β (fBasβπ)) |
129 | 1, 2, 128 | 3syl 18 |
1
β’ (π β πΏ β (fBasβπ)) |