Step | Hyp | Ref
| Expression |
1 | | pwrssmgc.5 |
. . . . . . 7
β’ (π β π β π΄) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π« π) β π β π΄) |
3 | | cnvimass 6038 |
. . . . . . . 8
β’ (β‘πΉ β π) β dom πΉ |
4 | | pwrssmgc.7 |
. . . . . . . 8
β’ (π β πΉ:πβΆπ) |
5 | 3, 4 | fssdm 6693 |
. . . . . . 7
β’ (π β (β‘πΉ β π) β π) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π« π) β (β‘πΉ β π) β π) |
7 | 2, 6 | sselpwd 5288 |
. . . . 5
β’ ((π β§ π β π« π) β (β‘πΉ β π) β π« π) |
8 | | pwrssmgc.1 |
. . . . 5
β’ πΊ = (π β π« π β¦ (β‘πΉ β π)) |
9 | 7, 8 | fmptd 7067 |
. . . 4
β’ (π β πΊ:π« πβΆπ« π) |
10 | | pwrssmgc.6 |
. . . . . 6
β’ (π β π β π΅) |
11 | | pwexg 5338 |
. . . . . 6
β’ (π β π΅ β π« π β V) |
12 | | pwrssmgc.3 |
. . . . . . 7
β’ π = (toIncβπ« π) |
13 | 12 | ipobas 18427 |
. . . . . 6
β’
(π« π β
V β π« π =
(Baseβπ)) |
14 | 10, 11, 13 | 3syl 18 |
. . . . 5
β’ (π β π« π = (Baseβπ)) |
15 | | pwexg 5338 |
. . . . . 6
β’ (π β π΄ β π« π β V) |
16 | | pwrssmgc.4 |
. . . . . . 7
β’ π = (toIncβπ« π) |
17 | 16 | ipobas 18427 |
. . . . . 6
β’
(π« π β
V β π« π =
(Baseβπ)) |
18 | 1, 15, 17 | 3syl 18 |
. . . . 5
β’ (π β π« π = (Baseβπ)) |
19 | 14, 18 | feq23d 6668 |
. . . 4
β’ (π β (πΊ:π« πβΆπ« π β πΊ:(Baseβπ)βΆ(Baseβπ))) |
20 | 9, 19 | mpbid 231 |
. . 3
β’ (π β πΊ:(Baseβπ)βΆ(Baseβπ)) |
21 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π« π) β π β π΅) |
22 | | ssrab2 4042 |
. . . . . . 7
β’ {π¦ β π β£ (β‘πΉ β {π¦}) β π} β π |
23 | 22 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π« π) β {π¦ β π β£ (β‘πΉ β {π¦}) β π} β π) |
24 | 21, 23 | sselpwd 5288 |
. . . . 5
β’ ((π β§ π β π« π) β {π¦ β π β£ (β‘πΉ β {π¦}) β π} β π« π) |
25 | | pwrssmgc.2 |
. . . . 5
β’ π» = (π β π« π β¦ {π¦ β π β£ (β‘πΉ β {π¦}) β π}) |
26 | 24, 25 | fmptd 7067 |
. . . 4
β’ (π β π»:π« πβΆπ« π) |
27 | 18, 14 | feq23d 6668 |
. . . 4
β’ (π β (π»:π« πβΆπ« π β π»:(Baseβπ)βΆ(Baseβπ))) |
28 | 26, 27 | mpbid 231 |
. . 3
β’ (π β π»:(Baseβπ)βΆ(Baseβπ)) |
29 | 20, 28 | jca 513 |
. 2
β’ (π β (πΊ:(Baseβπ)βΆ(Baseβπ) β§ π»:(Baseβπ)βΆ(Baseβπ))) |
30 | | sneq 4601 |
. . . . . . . . . . . 12
β’ (π¦ = π β {π¦} = {π}) |
31 | 30 | imaeq2d 6018 |
. . . . . . . . . . 11
β’ (π¦ = π β (β‘πΉ β {π¦}) = (β‘πΉ β {π})) |
32 | 31 | sseq1d 3980 |
. . . . . . . . . 10
β’ (π¦ = π β ((β‘πΉ β {π¦}) β π£ β (β‘πΉ β {π}) β π£)) |
33 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π’ β (Baseβπ)) |
34 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π« π = (Baseβπ)) |
35 | 33, 34 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π’ β π« π) |
36 | 35 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β π’ β π« π) |
37 | 36 | elpwid 4574 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β π’ β π) |
38 | 37 | sselda 3949 |
. . . . . . . . . 10
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β π β π) |
39 | 4 | ffund 6677 |
. . . . . . . . . . . . 13
β’ (π β Fun πΉ) |
40 | 39 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β Fun πΉ) |
41 | | snssi 4773 |
. . . . . . . . . . . . 13
β’ (π β π’ β {π} β π’) |
42 | 41 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β {π} β π’) |
43 | | sspreima 7023 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ {π} β π’) β (β‘πΉ β {π}) β (β‘πΉ β π’)) |
44 | 40, 42, 43 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β (β‘πΉ β {π}) β (β‘πΉ β π’)) |
45 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β (β‘πΉ β π’) β π£) |
46 | 44, 45 | sstrd 3959 |
. . . . . . . . . 10
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β (β‘πΉ β {π}) β π£) |
47 | 32, 38, 46 | elrabd 3652 |
. . . . . . . . 9
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β§ π β π’) β π β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
48 | 47 | ex 414 |
. . . . . . . 8
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β (π β π’ β π β {π¦ β π β£ (β‘πΉ β {π¦}) β π£})) |
49 | 48 | ssrdv 3955 |
. . . . . . 7
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ (β‘πΉ β π’) β π£) β π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
50 | | simplr 768 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
51 | 4 | ffnd 6674 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ Fn π) |
52 | 51 | ad4antr 731 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β πΉ Fn π) |
53 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β π β (β‘πΉ β π’)) |
54 | | elpreima 7013 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π β (π β (β‘πΉ β π’) β (π β π β§ (πΉβπ) β π’))) |
55 | 54 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((πΉ Fn π β§ π β (β‘πΉ β π’)) β (π β π β§ (πΉβπ) β π’)) |
56 | 52, 53, 55 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β (π β π β§ (πΉβπ) β π’)) |
57 | 56 | simprd 497 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β (πΉβπ) β π’) |
58 | 50, 57 | sseldd 3950 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β (πΉβπ) β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
59 | | sneq 4601 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (πΉβπ) β {π¦} = {(πΉβπ)}) |
60 | 59 | imaeq2d 6018 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΉβπ) β (β‘πΉ β {π¦}) = (β‘πΉ β {(πΉβπ)})) |
61 | 60 | sseq1d 3980 |
. . . . . . . . . . . . 13
β’ (π¦ = (πΉβπ) β ((β‘πΉ β {π¦}) β π£ β (β‘πΉ β {(πΉβπ)}) β π£)) |
62 | 61 | elrab 3650 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β {π¦ β π β£ (β‘πΉ β {π¦}) β π£} β ((πΉβπ) β π β§ (β‘πΉ β {(πΉβπ)}) β π£)) |
63 | 62 | simprbi 498 |
. . . . . . . . . . 11
β’ ((πΉβπ) β {π¦ β π β£ (β‘πΉ β {π¦}) β π£} β (β‘πΉ β {(πΉβπ)}) β π£) |
64 | 58, 63 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β (β‘πΉ β {(πΉβπ)}) β π£) |
65 | 56 | simpld 496 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β π β π) |
66 | | eqidd 2738 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β (πΉβπ) = (πΉβπ)) |
67 | | fniniseg 7015 |
. . . . . . . . . . . 12
β’ (πΉ Fn π β (π β (β‘πΉ β {(πΉβπ)}) β (π β π β§ (πΉβπ) = (πΉβπ)))) |
68 | 67 | biimpar 479 |
. . . . . . . . . . 11
β’ ((πΉ Fn π β§ (π β π β§ (πΉβπ) = (πΉβπ))) β π β (β‘πΉ β {(πΉβπ)})) |
69 | 52, 65, 66, 68 | syl12anc 836 |
. . . . . . . . . 10
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β π β (β‘πΉ β {(πΉβπ)})) |
70 | 64, 69 | sseldd 3950 |
. . . . . . . . 9
β’
(((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β§ π β (β‘πΉ β π’)) β π β π£) |
71 | 70 | ex 414 |
. . . . . . . 8
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β (π β (β‘πΉ β π’) β π β π£)) |
72 | 71 | ssrdv 3955 |
. . . . . . 7
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) β (β‘πΉ β π’) β π£) |
73 | 49, 72 | impbida 800 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β ((β‘πΉ β π’) β π£ β π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£})) |
74 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π = π’) β π = π’) |
75 | 74 | imaeq2d 6018 |
. . . . . . . 8
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π = π’) β (β‘πΉ β π) = (β‘πΉ β π’)) |
76 | 4, 1 | fexd 7182 |
. . . . . . . . . 10
β’ (π β πΉ β V) |
77 | | cnvexg 7866 |
. . . . . . . . . 10
β’ (πΉ β V β β‘πΉ β V) |
78 | | imaexg 7857 |
. . . . . . . . . 10
β’ (β‘πΉ β V β (β‘πΉ β π’) β V) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . 9
β’ (π β (β‘πΉ β π’) β V) |
80 | 79 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (β‘πΉ β π’) β V) |
81 | 8, 75, 35, 80 | fvmptd2 6961 |
. . . . . . 7
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (πΊβπ’) = (β‘πΉ β π’)) |
82 | 81 | sseq1d 3980 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β ((πΊβπ’) β π£ β (β‘πΉ β π’) β π£)) |
83 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π = π£) β π = π£) |
84 | 83 | sseq2d 3981 |
. . . . . . . . 9
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π = π£) β ((β‘πΉ β {π¦}) β π β (β‘πΉ β {π¦}) β π£)) |
85 | 84 | rabbidv 3418 |
. . . . . . . 8
β’ ((((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β§ π = π£) β {π¦ β π β£ (β‘πΉ β {π¦}) β π} = {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
86 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π£ β (Baseβπ)) |
87 | 1, 15 | syl 17 |
. . . . . . . . . . 11
β’ (π β π« π β V) |
88 | 87 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π« π β V) |
89 | 88, 17 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π« π = (Baseβπ)) |
90 | 86, 89 | eleqtrrd 2841 |
. . . . . . . 8
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π£ β π« π) |
91 | 10 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π β π΅) |
92 | | ssrab2 4042 |
. . . . . . . . . 10
β’ {π¦ β π β£ (β‘πΉ β {π¦}) β π£} β π |
93 | 92 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β {π¦ β π β£ (β‘πΉ β {π¦}) β π£} β π) |
94 | 91, 93 | sselpwd 5288 |
. . . . . . . 8
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β {π¦ β π β£ (β‘πΉ β {π¦}) β π£} β π« π) |
95 | 25, 85, 90, 94 | fvmptd2 6961 |
. . . . . . 7
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (π»βπ£) = {π¦ β π β£ (β‘πΉ β {π¦}) β π£}) |
96 | 95 | sseq2d 3981 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (π’ β (π»βπ£) β π’ β {π¦ β π β£ (β‘πΉ β {π¦}) β π£})) |
97 | 73, 82, 96 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β ((πΊβπ’) β π£ β π’ β (π»βπ£))) |
98 | 9 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β πΊ:π« πβΆπ« π) |
99 | 98, 35 | ffvelcdmd 7041 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (πΊβπ’) β π« π) |
100 | | eqid 2737 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
101 | 16, 100 | ipole 18430 |
. . . . . 6
β’
((π« π β
V β§ (πΊβπ’) β π« π β§ π£ β π« π) β ((πΊβπ’)(leβπ)π£ β (πΊβπ’) β π£)) |
102 | 88, 99, 90, 101 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β ((πΊβπ’)(leβπ)π£ β (πΊβπ’) β π£)) |
103 | 10, 11 | syl 17 |
. . . . . . 7
β’ (π β π« π β V) |
104 | 103 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π« π β V) |
105 | 26 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β π»:π« πβΆπ« π) |
106 | 105, 90 | ffvelcdmd 7041 |
. . . . . 6
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (π»βπ£) β π« π) |
107 | | eqid 2737 |
. . . . . . 7
β’
(leβπ) =
(leβπ) |
108 | 12, 107 | ipole 18430 |
. . . . . 6
β’
((π« π β
V β§ π’ β π«
π β§ (π»βπ£) β π« π) β (π’(leβπ)(π»βπ£) β π’ β (π»βπ£))) |
109 | 104, 35, 106, 108 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β (π’(leβπ)(π»βπ£) β π’ β (π»βπ£))) |
110 | 97, 102, 109 | 3bitr4d 311 |
. . . 4
β’ (((π β§ π’ β (Baseβπ)) β§ π£ β (Baseβπ)) β ((πΊβπ’)(leβπ)π£ β π’(leβπ)(π»βπ£))) |
111 | 110 | anasss 468 |
. . 3
β’ ((π β§ (π’ β (Baseβπ) β§ π£ β (Baseβπ))) β ((πΊβπ’)(leβπ)π£ β π’(leβπ)(π»βπ£))) |
112 | 111 | ralrimivva 3198 |
. 2
β’ (π β βπ’ β (Baseβπ)βπ£ β (Baseβπ)((πΊβπ’)(leβπ)π£ β π’(leβπ)(π»βπ£))) |
113 | | eqid 2737 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
114 | | eqid 2737 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
115 | | eqid 2737 |
. . 3
β’ (πMGalConnπ) = (πMGalConnπ) |
116 | 12 | ipopos 18432 |
. . . 4
β’ π β Poset |
117 | | posprs 18212 |
. . . 4
β’ (π β Poset β π β Proset
) |
118 | 116, 117 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
119 | 16 | ipopos 18432 |
. . . 4
β’ π β Poset |
120 | | posprs 18212 |
. . . 4
β’ (π β Poset β π β Proset
) |
121 | 119, 120 | mp1i 13 |
. . 3
β’ (π β π β Proset ) |
122 | 113, 114,
107, 100, 115, 118, 121 | mgcval 31889 |
. 2
β’ (π β (πΊ(πMGalConnπ)π» β ((πΊ:(Baseβπ)βΆ(Baseβπ) β§ π»:(Baseβπ)βΆ(Baseβπ)) β§ βπ’ β (Baseβπ)βπ£ β (Baseβπ)((πΊβπ’)(leβπ)π£ β π’(leβπ)(π»βπ£))))) |
123 | 29, 112, 122 | mpbir2and 712 |
1
β’ (π β πΊ(πMGalConnπ)π») |