Step | Hyp | Ref
| Expression |
1 | | nsgqusf1o.f |
. . . . 5
β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) |
2 | 1 | elrnmpt 5916 |
. . . 4
β’ (β β V β (β β ran πΉ β βπ β π β = {π β π΅ β£ ({π} β π) β π})) |
3 | 2 | elv 3454 |
. . 3
β’ (β β ran πΉ β βπ β π β = {π β π΅ β£ ({π} β π) β π}) |
4 | | nsgqusf1o.s |
. . . . 5
β’ π = {β β (SubGrpβπΊ) β£ π β β} |
5 | 4 | reqabi 3432 |
. . . 4
β’ (β β π β (β β (SubGrpβπΊ) β§ π β β)) |
6 | | nsgqusf1o.b |
. . . . . . . 8
β’ π΅ = (BaseβπΊ) |
7 | | nsgqusf1o.t |
. . . . . . . 8
β’ π = (SubGrpβπ) |
8 | | nsgqusf1o.1 |
. . . . . . . 8
β’ β€ =
(leβ(toIncβπ)) |
9 | | nsgqusf1o.2 |
. . . . . . . 8
β’ β² =
(leβ(toIncβπ)) |
10 | | nsgqusf1o.q |
. . . . . . . 8
β’ π = (πΊ /s (πΊ ~QG π)) |
11 | | nsgqusf1o.p |
. . . . . . . 8
β’ β =
(LSSumβπΊ) |
12 | | nsgqusf1o.e |
. . . . . . . 8
β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) |
13 | | nsgqusf1o.n |
. . . . . . . 8
β’ (π β π β (NrmSGrpβπΊ)) |
14 | 6, 4, 7, 8, 9, 10,
11, 12, 1, 13 | nsgqusf1olem1 32231 |
. . . . . . 7
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) |
15 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π = ran (π₯ β β β¦ ({π₯} β π)) β (({π} β π) β π β ({π} β π) β ran (π₯ β β β¦ ({π₯} β π)))) |
16 | 15 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = ran (π₯ β β β¦ ({π₯} β π)) β {π β π΅ β£ ({π} β π) β π} = {π β π΅ β£ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))}) |
17 | 16 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = ran (π₯ β β β¦ ({π₯} β π)) β (β = {π β π΅ β£ ({π} β π) β π} β β = {π β π΅ β£ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))})) |
18 | 17 | adantl 483 |
. . . . . . 7
β’ ((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π = ran (π₯ β β β¦ ({π₯} β π))) β (β = {π β π΅ β£ ({π} β π) β π} β β = {π β π΅ β£ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))})) |
19 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π₯(((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) |
20 | | nfmpt1 5218 |
. . . . . . . . . . . . . 14
β’
β²π₯(π₯ β β β¦ ({π₯} β π)) |
21 | 20 | nfrn 5912 |
. . . . . . . . . . . . 13
β’
β²π₯ran
(π₯ β β β¦ ({π₯} β π)) |
22 | 21 | nfel2 2926 |
. . . . . . . . . . . 12
β’
β²π₯({π} β π) β ran (π₯ β β β¦ ({π₯} β π)) |
23 | 19, 22 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π₯((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) |
24 | | nsgsubg 18967 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
25 | 13, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (SubGrpβπΊ)) |
26 | | subgrcl 18940 |
. . . . . . . . . . . . . . . . 17
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΊ β Grp) |
28 | 27 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β πΊ β Grp) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β πΊ β Grp) |
30 | 6 | subgss 18936 |
. . . . . . . . . . . . . . . . 17
β’ (β β (SubGrpβπΊ) β β β π΅) |
31 | 30 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β β β π΅) |
32 | 31 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β π₯ β π΅) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π₯ β π΅) |
34 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β π β π΅) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π β π΅) |
36 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(+gβπΊ) = (+gβπΊ) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(invgβπΊ) = (invgβπΊ) |
38 | 6, 36, 37 | grpasscan1 18817 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π₯ β π΅ β§ π β π΅) β (π₯(+gβπΊ)(((invgβπΊ)βπ₯)(+gβπΊ)π)) = π) |
39 | 29, 33, 35, 38 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β (π₯(+gβπΊ)(((invgβπΊ)βπ₯)(+gβπΊ)π)) = π) |
40 | | simp-5r 785 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β β β (SubGrpβπΊ)) |
41 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π₯ β β) |
42 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π β β) |
43 | 6 | subgss 18936 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (SubGrpβπΊ) β π β π΅) |
44 | 25, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π΅) |
45 | 44 | ad5antr 733 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π β π΅) |
46 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΊ ~QG π) = (πΊ ~QG π) |
47 | 6, 46 | eqger 18987 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (SubGrpβπΊ) β (πΊ ~QG π) Er π΅) |
48 | 25, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΊ ~QG π) Er π΅) |
49 | 48 | ad4antr 731 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β (πΊ ~QG π) Er π΅) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β (πΊ ~QG π) Er π΅) |
51 | 49, 34 | erth 8704 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β (π(πΊ ~QG π)π₯ β [π](πΊ ~QG π) = [π₯](πΊ ~QG π))) |
52 | 25 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β π β (SubGrpβπΊ)) |
53 | 6, 11, 52, 34 | quslsm 32226 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β [π](πΊ ~QG π) = ({π} β π)) |
54 | 6, 11, 52, 32 | quslsm 32226 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β [π₯](πΊ ~QG π) = ({π₯} β π)) |
55 | 53, 54 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β ([π](πΊ ~QG π) = [π₯](πΊ ~QG π) β ({π} β π) = ({π₯} β π))) |
56 | 51, 55 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β (π(πΊ ~QG π)π₯ β ({π} β π) = ({π₯} β π))) |
57 | 56 | biimpar 479 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π(πΊ ~QG π)π₯) |
58 | 50, 57 | ersym 8667 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π₯(πΊ ~QG π)π) |
59 | 6, 37, 36, 46 | eqgval 18986 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β Grp β§ π β π΅) β (π₯(πΊ ~QG π)π β (π₯ β π΅ β§ π β π΅ β§ (((invgβπΊ)βπ₯)(+gβπΊ)π) β π))) |
60 | 59 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊ β Grp β§ π β π΅) β§ π₯(πΊ ~QG π)π) β (π₯ β π΅ β§ π β π΅ β§ (((invgβπΊ)βπ₯)(+gβπΊ)π) β π)) |
61 | 60 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β Grp β§ π β π΅) β§ π₯(πΊ ~QG π)π) β (((invgβπΊ)βπ₯)(+gβπΊ)π) β π) |
62 | 29, 45, 58, 61 | syl21anc 837 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β (((invgβπΊ)βπ₯)(+gβπΊ)π) β π) |
63 | 42, 62 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β (((invgβπΊ)βπ₯)(+gβπΊ)π) β β) |
64 | 36 | subgcl 18945 |
. . . . . . . . . . . . . 14
β’ ((β β (SubGrpβπΊ) β§ π₯ β β β§ (((invgβπΊ)βπ₯)(+gβπΊ)π) β β) β (π₯(+gβπΊ)(((invgβπΊ)βπ₯)(+gβπΊ)π)) β β) |
65 | 40, 41, 63, 64 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β (π₯(+gβπΊ)(((invgβπΊ)βπ₯)(+gβπΊ)π)) β β) |
66 | 39, 65 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π β β) |
67 | 66 | adantllr 718 |
. . . . . . . . . . 11
β’
(((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) β§ π₯ β β) β§ ({π} β π) = ({π₯} β π)) β π β β) |
68 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β¦ ({π₯} β π)) = (π₯ β β β¦ ({π₯} β π)) |
69 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ ({π₯} β π) β V |
70 | 68, 69 | elrnmpti 5920 |
. . . . . . . . . . . . 13
β’ (({π} β π) β ran (π₯ β β β¦ ({π₯} β π)) β βπ₯ β β ({π} β π) = ({π₯} β π)) |
71 | 70 | biimpi 215 |
. . . . . . . . . . . 12
β’ (({π} β π) β ran (π₯ β β β¦ ({π₯} β π)) β βπ₯ β β ({π} β π) = ({π₯} β π)) |
72 | 71 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) β βπ₯ β β ({π} β π) = ({π₯} β π)) |
73 | 23, 67, 72 | r19.29af 3254 |
. . . . . . . . . 10
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) β π β β) |
74 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π β β) β π β β) |
75 | | ovexd 7397 |
. . . . . . . . . . 11
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π β β) β ({π} β π) β V) |
76 | | sneq 4601 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β {π₯} = {π}) |
77 | 76 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ({π₯} β π) = ({π} β π)) |
78 | 77 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (π₯ = π β ({π} β π) = ({π₯} β π)) |
79 | 78 | adantl 483 |
. . . . . . . . . . 11
β’
((((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π β β) β§ π₯ = π) β ({π} β π) = ({π₯} β π)) |
80 | 68, 74, 75, 79 | elrnmptdv 5922 |
. . . . . . . . . 10
β’
(((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β§ π β β) β ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))) |
81 | 73, 80 | impbida 800 |
. . . . . . . . 9
β’ ((((π β§ β β (SubGrpβπΊ)) β§ π β β) β§ π β π΅) β (({π} β π) β ran (π₯ β β β¦ ({π₯} β π)) β π β β)) |
82 | 81 | rabbidva 3417 |
. . . . . . . 8
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β {π β π΅ β£ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))} = {π β π΅ β£ π β β}) |
83 | 30 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ β β (SubGrpβπΊ)) β β β π΅) |
84 | | dfss7 4205 |
. . . . . . . . . 10
β’ (β β π΅ β {π β π΅ β£ π β β} = β) |
85 | 83, 84 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ β β (SubGrpβπΊ)) β {π β π΅ β£ π β β} = β) |
86 | 85 | adantr 482 |
. . . . . . . 8
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β {π β π΅ β£ π β β} = β) |
87 | 82, 86 | eqtr2d 2778 |
. . . . . . 7
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β β = {π β π΅ β£ ({π} β π) β ran (π₯ β β β¦ ({π₯} β π))}) |
88 | 14, 18, 87 | rspcedvd 3586 |
. . . . . 6
β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β βπ β π β = {π β π΅ β£ ({π} β π) β π}) |
89 | 88 | anasss 468 |
. . . . 5
β’ ((π β§ (β β (SubGrpβπΊ) β§ π β β)) β βπ β π β = {π β π΅ β£ ({π} β π) β π}) |
90 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β (NrmSGrpβπΊ)) |
91 | 7 | eleq2i 2830 |
. . . . . . . . . . . 12
β’ (π β π β π β (SubGrpβπ)) |
92 | 91 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π β π β (SubGrpβπ)) |
93 | 92 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β (SubGrpβπ)) |
94 | 6, 10, 11, 90, 93 | nsgmgclem 32229 |
. . . . . . . . 9
β’ ((π β§ π β π) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ)) |
95 | 94 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ)) |
96 | | eleq1 2826 |
. . . . . . . . 9
β’ (β = {π β π΅ β£ ({π} β π) β π} β (β β (SubGrpβπΊ) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ))) |
97 | 96 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β (β β (SubGrpβπΊ) β {π β π΅ β£ ({π} β π) β π} β (SubGrpβπΊ))) |
98 | 95, 97 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β β β (SubGrpβπΊ)) |
99 | 44 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π΅) |
100 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π) β π β (SubGrpβπΊ)) |
101 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π) β π β π) |
102 | 11 | grplsmid 32225 |
. . . . . . . . . . . 12
β’ ((π β (SubGrpβπΊ) β§ π β π) β ({π} β π) = π) |
103 | 100, 101,
102 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β ({π} β π) = π) |
104 | 10 | nsgqus0 32228 |
. . . . . . . . . . . . 13
β’ ((π β (NrmSGrpβπΊ) β§ π β (SubGrpβπ)) β π β π) |
105 | 90, 93, 104 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β π) |
106 | 105 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π) β π β π) |
107 | 103, 106 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β π) β ({π} β π) β π) |
108 | 99, 107 | ssrabdv 4036 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β {π β π΅ β£ ({π} β π) β π}) |
109 | 108 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β π β {π β π΅ β£ ({π} β π) β π}) |
110 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β β = {π β π΅ β£ ({π} β π) β π}) |
111 | 109, 110 | sseqtrrd 3990 |
. . . . . . 7
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β π β β) |
112 | 98, 111 | jca 513 |
. . . . . 6
β’ (((π β§ π β π) β§ β = {π β π΅ β£ ({π} β π) β π}) β (β β (SubGrpβπΊ) β§ π β β)) |
113 | 112 | r19.29an 3156 |
. . . . 5
β’ ((π β§ βπ β π β = {π β π΅ β£ ({π} β π) β π}) β (β β (SubGrpβπΊ) β§ π β β)) |
114 | 89, 113 | impbida 800 |
. . . 4
β’ (π β ((β β (SubGrpβπΊ) β§ π β β) β βπ β π β = {π β π΅ β£ ({π} β π) β π})) |
115 | 5, 114 | bitrid 283 |
. . 3
β’ (π β (β β π β βπ β π β = {π β π΅ β£ ({π} β π) β π})) |
116 | 3, 115 | bitr4id 290 |
. 2
β’ (π β (β β ran πΉ β β β π)) |
117 | 116 | eqrdv 2735 |
1
β’ (π β ran πΉ = π) |