Step | Hyp | Ref
| Expression |
1 | | submrcl 17346 |
. . . . . 6
SubMnd
|
2 | | eqid 2622 |
. . . . . . 7
|
3 | | eqid 2622 |
. . . . . . 7
|
4 | | eqid 2622 |
. . . . . . 7
.g .g |
5 | | eqid 2622 |
. . . . . . 7
|
6 | | eqid 2622 |
. . . . . . 7
|
7 | 2, 3, 4, 5, 6 | isarchi2 29739 |
. . . . . 6
Toset
Archi
.g |
8 | 1, 7 | sylan2 491 |
. . . . 5
Toset
SubMnd
Archi
.g |
9 | 8 | biimpa 501 |
. . . 4
Toset SubMnd
Archi
.g |
10 | 9 | an32s 846 |
. . 3
Toset Archi SubMnd
.g |
11 | | eqid 2622 |
. . . . . . . 8
↾s ↾s |
12 | 11 | submbas 17355 |
. . . . . . 7
SubMnd
↾s |
13 | 2 | submss 17350 |
. . . . . . 7
SubMnd
|
14 | 12, 13 | eqsstr3d 3640 |
. . . . . 6
SubMnd
↾s |
15 | | ssralv 3666 |
. . . . . . . 8
↾s
.g ↾s
.g |
16 | 15 | ralimdv 2963 |
. . . . . . 7
↾s
.g ↾s
.g |
17 | | ssralv 3666 |
. . . . . . 7
↾s ↾s
.g ↾s
↾s
.g |
18 | 16, 17 | syld 47 |
. . . . . 6
↾s
.g ↾s
↾s
.g |
19 | 14, 18 | syl 17 |
. . . . 5
SubMnd
.g ↾s
↾s
.g |
20 | 19 | adantl 482 |
. . . 4
Toset Archi SubMnd
.g ↾s
↾s
.g |
21 | 11, 3 | subm0 17356 |
. . . . . . . . . 10
SubMnd
↾s |
22 | 21 | ad2antrr 762 |
. . . . . . . . 9
SubMnd ↾s ↾s ↾s |
23 | 11, 5 | ressle 16059 |
. . . . . . . . . . . 12
SubMnd
↾s |
24 | 23 | difeq1d 3727 |
. . . . . . . . . . 11
SubMnd
↾s |
25 | 5, 6 | pltfval 16959 |
. . . . . . . . . . . 12
|
26 | 1, 25 | syl 17 |
. . . . . . . . . . 11
SubMnd
|
27 | 11 | submmnd 17354 |
. . . . . . . . . . . 12
SubMnd
↾s |
28 | | eqid 2622 |
. . . . . . . . . . . . 13
↾s ↾s |
29 | | eqid 2622 |
. . . . . . . . . . . . 13
↾s ↾s |
30 | 28, 29 | pltfval 16959 |
. . . . . . . . . . . 12
↾s ↾s
↾s |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
SubMnd
↾s
↾s |
32 | 24, 26, 31 | 3eqtr4d 2666 |
. . . . . . . . . 10
SubMnd
↾s |
33 | 32 | ad2antrr 762 |
. . . . . . . . 9
SubMnd ↾s ↾s ↾s |
34 | | eqidd 2623 |
. . . . . . . . 9
SubMnd ↾s ↾s
|
35 | 22, 33, 34 | breq123d 4667 |
. . . . . . . 8
SubMnd ↾s ↾s ↾s ↾s |
36 | | eqidd 2623 |
. . . . . . . . . 10
SubMnd
↾s ↾s |
37 | 23 | ad3antrrr 766 |
. . . . . . . . . 10
SubMnd
↾s ↾s ↾s |
38 | | simplll 798 |
. . . . . . . . . . 11
SubMnd
↾s ↾s SubMnd |
39 | | simpr 477 |
. . . . . . . . . . . 12
SubMnd
↾s ↾s |
40 | 39 | nnnn0d 11351 |
. . . . . . . . . . 11
SubMnd
↾s ↾s |
41 | | simpllr 799 |
. . . . . . . . . . . 12
SubMnd
↾s ↾s ↾s |
42 | 38, 12 | syl 17 |
. . . . . . . . . . . 12
SubMnd
↾s ↾s ↾s |
43 | 41, 42 | eleqtrrd 2704 |
. . . . . . . . . . 11
SubMnd
↾s ↾s |
44 | | eqid 2622 |
. . . . . . . . . . . 12
.g ↾s .g ↾s |
45 | 4, 11, 44 | submmulg 17586 |
. . . . . . . . . . 11
SubMnd .g .g ↾s |
46 | 38, 40, 43, 45 | syl3anc 1326 |
. . . . . . . . . 10
SubMnd
↾s ↾s .g .g
↾s |
47 | 36, 37, 46 | breq123d 4667 |
. . . . . . . . 9
SubMnd
↾s ↾s .g
↾s .g
↾s |
48 | 47 | rexbidva 3049 |
. . . . . . . 8
SubMnd ↾s ↾s .g
↾s .g ↾s |
49 | 35, 48 | imbi12d 334 |
. . . . . . 7
SubMnd ↾s ↾s
.g
↾s
↾s
↾s .g ↾s |
50 | 49 | ralbidva 2985 |
. . . . . 6
SubMnd ↾s ↾s
.g
↾s ↾s ↾s
↾s .g ↾s |
51 | 50 | ralbidva 2985 |
. . . . 5
SubMnd
↾s
↾s
.g
↾s
↾s ↾s ↾s
↾s .g ↾s |
52 | 51 | adantl 482 |
. . . 4
Toset Archi SubMnd
↾s
↾s
.g
↾s
↾s ↾s ↾s
↾s .g ↾s |
53 | 20, 52 | sylibd 229 |
. . 3
Toset Archi SubMnd
.g ↾s
↾s ↾s ↾s
↾s .g ↾s |
54 | 10, 53 | mpd 15 |
. 2
Toset Archi SubMnd
↾s
↾s ↾s ↾s
↾s .g ↾s |
55 | | resstos 29660 |
. . . 4
Toset
SubMnd
↾s
Toset |
56 | 27 | adantl 482 |
. . . 4
Toset
SubMnd
↾s |
57 | | eqid 2622 |
. . . . 5
↾s ↾s |
58 | | eqid 2622 |
. . . . 5
↾s ↾s |
59 | 57, 58, 44, 28, 29 | isarchi2 29739 |
. . . 4
↾s Toset ↾s ↾s Archi
↾s ↾s ↾s ↾s
↾s .g ↾s |
60 | 55, 56, 59 | syl2anc 693 |
. . 3
Toset
SubMnd
↾s Archi
↾s
↾s ↾s ↾s
↾s .g ↾s |
61 | 60 | adantlr 751 |
. 2
Toset Archi SubMnd
↾s Archi
↾s
↾s ↾s ↾s
↾s .g ↾s |
62 | 54, 61 | mpbird 247 |
1
Toset Archi SubMnd
↾s
Archi |