Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . 8
SalGen SalGen |
2 | 1 | eqcomd 2628 |
. . . . . . 7
SalGen SalGen |
3 | 2 | adantl 482 |
. . . . . 6
SalGen SalGen |
4 | | dfsalgen2.1 |
. . . . . . . 8
|
5 | | salgencl 40550 |
. . . . . . . 8
SalGen SAlg |
6 | 4, 5 | syl 17 |
. . . . . . 7
SalGen SAlg |
7 | 6 | adantr 481 |
. . . . . 6
SalGen SalGen SAlg |
8 | 3, 7 | eqeltrd 2701 |
. . . . 5
SalGen SAlg |
9 | | unieq 4444 |
. . . . . . 7
SalGen SalGen |
10 | 9 | adantl 482 |
. . . . . 6
SalGen SalGen |
11 | 4 | adantr 481 |
. . . . . . 7
SalGen |
12 | | eqid 2622 |
. . . . . . 7
SalGen SalGen |
13 | | eqid 2622 |
. . . . . . 7
|
14 | 11, 12, 13 | salgenuni 40555 |
. . . . . 6
SalGen SalGen |
15 | 10, 14 | eqtr3d 2658 |
. . . . 5
SalGen |
16 | 12 | sssalgen 40553 |
. . . . . . 7
SalGen |
17 | 11, 16 | syl 17 |
. . . . . 6
SalGen SalGen |
18 | | simpr 477 |
. . . . . 6
SalGen SalGen |
19 | 17, 18 | sseqtrd 3641 |
. . . . 5
SalGen |
20 | 8, 15, 19 | 3jca 1242 |
. . . 4
SalGen SAlg |
21 | 3 | ad2antrr 762 |
. . . . . . . 8
SalGen SAlg SalGen |
22 | 21 | adantrl 752 |
. . . . . . 7
SalGen SAlg
SalGen |
23 | 11 | ad2antrr 762 |
. . . . . . . . 9
SalGen SAlg |
24 | 23 | adantrl 752 |
. . . . . . . 8
SalGen SAlg
|
25 | | simplr 792 |
. . . . . . . . 9
SalGen SAlg SAlg |
26 | 25 | adantrl 752 |
. . . . . . . 8
SalGen SAlg
SAlg |
27 | | simpr 477 |
. . . . . . . . 9
SalGen SAlg |
28 | 27 | adantrl 752 |
. . . . . . . 8
SalGen SAlg
|
29 | | simprl 794 |
. . . . . . . 8
SalGen SAlg
|
30 | 24, 12, 26, 28, 29 | salgenss 40554 |
. . . . . . 7
SalGen SAlg
SalGen |
31 | 22, 30 | eqsstrd 3639 |
. . . . . 6
SalGen SAlg
|
32 | 31 | ex 450 |
. . . . 5
SalGen SAlg
|
33 | 32 | ralrimiva 2966 |
. . . 4
SalGen SAlg |
34 | 20, 33 | jca 554 |
. . 3
SalGen SAlg
SAlg
|
35 | 34 | ex 450 |
. 2
SalGen SAlg
SAlg |
36 | 4 | adantr 481 |
. . . 4
SAlg
SAlg
|
37 | | simprl1 1106 |
. . . 4
SAlg
SAlg
SAlg |
38 | | simprl2 1107 |
. . . 4
SAlg
SAlg
|
39 | | simprl3 1108 |
. . . 4
SAlg
SAlg
|
40 | | unieq 4444 |
. . . . . . . . . . . . . . 15
|
41 | 40 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
42 | | sseq2 3627 |
. . . . . . . . . . . . . 14
|
43 | 41, 42 | anbi12d 747 |
. . . . . . . . . . . . 13
|
44 | | sseq2 3627 |
. . . . . . . . . . . . 13
|
45 | 43, 44 | imbi12d 334 |
. . . . . . . . . . . 12
|
46 | 45 | cbvralv 3171 |
. . . . . . . . . . 11
SAlg
SAlg |
47 | 46 | biimpi 206 |
. . . . . . . . . 10
SAlg
SAlg |
48 | 47 | adantr 481 |
. . . . . . . . 9
SAlg SAlg
SAlg |
49 | | simpr 477 |
. . . . . . . . 9
SAlg SAlg
SAlg |
50 | 48, 49 | jca 554 |
. . . . . . . 8
SAlg SAlg
SAlg
SAlg |
51 | 50 | 3ad2antr1 1226 |
. . . . . . 7
SAlg SAlg
SAlg SAlg |
52 | | 3simpc 1060 |
. . . . . . . 8
SAlg
|
53 | 52 | adantl 482 |
. . . . . . 7
SAlg SAlg
|
54 | | rspa 2930 |
. . . . . . 7
SAlg SAlg
|
55 | 51, 53, 54 | sylc 65 |
. . . . . 6
SAlg SAlg
|
56 | 55 | adantll 750 |
. . . . 5
SAlg
SAlg
SAlg
|
57 | 56 | adantll 750 |
. . . 4
SAlg
SAlg SAlg |
58 | 36, 37, 38, 39, 57 | issalgend 40556 |
. . 3
SAlg
SAlg
SalGen |
59 | 58 | ex 450 |
. 2
SAlg
SAlg
SalGen |
60 | 35, 59 | impbid 202 |
1
SalGen
SAlg
SAlg
|