Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . 8
β’
((SalGenβπ) =
π β
(SalGenβπ) = π) |
2 | 1 | eqcomd 2738 |
. . . . . . 7
β’
((SalGenβπ) =
π β π = (SalGenβπ)) |
3 | 2 | adantl 483 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β π = (SalGenβπ)) |
4 | | dfsalgen2.1 |
. . . . . . . 8
β’ (π β π β π) |
5 | | salgencl 44663 |
. . . . . . . 8
β’ (π β π β (SalGenβπ) β SAlg) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (π β (SalGenβπ) β SAlg) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β (SalGenβπ) β SAlg) |
8 | 3, 7 | eqeltrd 2833 |
. . . . 5
β’ ((π β§ (SalGenβπ) = π) β π β SAlg) |
9 | | unieq 4880 |
. . . . . . 7
β’
((SalGenβπ) =
π β βͺ (SalGenβπ) = βͺ π) |
10 | 9 | adantl 483 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β βͺ
(SalGenβπ) = βͺ π) |
11 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ (SalGenβπ) = π) β π β π) |
12 | | eqid 2732 |
. . . . . . 7
β’
(SalGenβπ) =
(SalGenβπ) |
13 | | eqid 2732 |
. . . . . . 7
β’ βͺ π =
βͺ π |
14 | 11, 12, 13 | salgenuni 44668 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β βͺ
(SalGenβπ) = βͺ π) |
15 | 10, 14 | eqtr3d 2774 |
. . . . 5
β’ ((π β§ (SalGenβπ) = π) β βͺ π = βͺ
π) |
16 | 12 | sssalgen 44666 |
. . . . . . 7
β’ (π β π β π β (SalGenβπ)) |
17 | 11, 16 | syl 17 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β π β (SalGenβπ)) |
18 | | simpr 486 |
. . . . . 6
β’ ((π β§ (SalGenβπ) = π) β (SalGenβπ) = π) |
19 | 17, 18 | sseqtrd 3988 |
. . . . 5
β’ ((π β§ (SalGenβπ) = π) β π β π) |
20 | 8, 15, 19 | 3jca 1129 |
. . . 4
β’ ((π β§ (SalGenβπ) = π) β (π β SAlg β§ βͺ π =
βͺ π β§ π β π)) |
21 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ π β π¦) β π = (SalGenβπ)) |
22 | 21 | adantrl 715 |
. . . . . . 7
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β π = (SalGenβπ)) |
23 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ π β π¦) β π β π) |
24 | 23 | adantrl 715 |
. . . . . . . 8
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β π β π) |
25 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ π β π¦) β π¦ β SAlg) |
26 | 25 | adantrl 715 |
. . . . . . . 8
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β π¦ β SAlg) |
27 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ π β π¦) β π β π¦) |
28 | 27 | adantrl 715 |
. . . . . . . 8
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β π β π¦) |
29 | | simprl 770 |
. . . . . . . 8
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β βͺ π¦ = βͺ
π) |
30 | 24, 12, 26, 28, 29 | salgenss 44667 |
. . . . . . 7
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β (SalGenβπ) β π¦) |
31 | 22, 30 | eqsstrd 3986 |
. . . . . 6
β’ ((((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β§ (βͺ π¦ =
βͺ π β§ π β π¦)) β π β π¦) |
32 | 31 | ex 414 |
. . . . 5
β’ (((π β§ (SalGenβπ) = π) β§ π¦ β SAlg) β ((βͺ π¦ =
βͺ π β§ π β π¦) β π β π¦)) |
33 | 32 | ralrimiva 3140 |
. . . 4
β’ ((π β§ (SalGenβπ) = π) β βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦)) |
34 | 20, 33 | jca 513 |
. . 3
β’ ((π β§ (SalGenβπ) = π) β ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) |
35 | 34 | ex 414 |
. 2
β’ (π β ((SalGenβπ) = π β ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦)))) |
36 | 4 | adantr 482 |
. . . 4
β’ ((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β π β π) |
37 | | simprl1 1219 |
. . . 4
β’ ((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β π β SAlg) |
38 | | simprl2 1220 |
. . . 4
β’ ((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β βͺ π = βͺ
π) |
39 | | simprl3 1221 |
. . . 4
β’ ((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β π β π) |
40 | | unieq 4880 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π€ β βͺ π¦ = βͺ
π€) |
41 | 40 | eqeq1d 2734 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β (βͺ π¦ = βͺ
π β βͺ π€ =
βͺ π)) |
42 | | sseq2 3974 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β (π β π¦ β π β π€)) |
43 | 41, 42 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β ((βͺ π¦ = βͺ
π β§ π β π¦) β (βͺ π€ = βͺ
π β§ π β π€))) |
44 | | sseq2 3974 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β (π β π¦ β π β π€)) |
45 | 43, 44 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β (((βͺ π¦ = βͺ
π β§ π β π¦) β π β π¦) β ((βͺ π€ = βͺ
π β§ π β π€) β π β π€))) |
46 | 45 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β βπ€ β SAlg ((βͺ
π€ = βͺ π
β§ π β π€) β π β π€)) |
47 | 46 | biimpi 215 |
. . . . . . . . . 10
β’
(βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β βπ€ β SAlg ((βͺ
π€ = βͺ π
β§ π β π€) β π β π€)) |
48 | 47 | adantr 482 |
. . . . . . . . 9
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ π€ β SAlg) β βπ€ β SAlg ((βͺ π€ =
βͺ π β§ π β π€) β π β π€)) |
49 | | simpr 486 |
. . . . . . . . 9
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ π€ β SAlg) β π€ β SAlg) |
50 | 48, 49 | jca 513 |
. . . . . . . 8
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ π€ β SAlg) β (βπ€ β SAlg ((βͺ π€ =
βͺ π β§ π β π€) β π β π€) β§ π€ β SAlg)) |
51 | 50 | 3ad2antr1 1189 |
. . . . . . 7
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ (π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€)) β (βπ€ β SAlg ((βͺ
π€ = βͺ π
β§ π β π€) β π β π€) β§ π€ β SAlg)) |
52 | | 3simpc 1151 |
. . . . . . . 8
β’ ((π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€) β (βͺ π€ = βͺ
π β§ π β π€)) |
53 | 52 | adantl 483 |
. . . . . . 7
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ (π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€)) β (βͺ π€ = βͺ
π β§ π β π€)) |
54 | | rspa 3230 |
. . . . . . 7
β’
((βπ€ β
SAlg ((βͺ π€ = βͺ π β§ π β π€) β π β π€) β§ π€ β SAlg) β ((βͺ π€ =
βͺ π β§ π β π€) β π β π€)) |
55 | 51, 53, 54 | sylc 65 |
. . . . . 6
β’
((βπ¦ β
SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦) β§ (π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€)) β π β π€) |
56 | 55 | adantll 713 |
. . . . 5
β’ ((((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦)) β§ (π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€)) β π β π€) |
57 | 56 | adantll 713 |
. . . 4
β’ (((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β§ (π€ β SAlg β§ βͺ π€ =
βͺ π β§ π β π€)) β π β π€) |
58 | 36, 37, 38, 39, 57 | issalgend 44669 |
. . 3
β’ ((π β§ ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦))) β (SalGenβπ) = π) |
59 | 58 | ex 414 |
. 2
β’ (π β (((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦)) β (SalGenβπ) = π)) |
60 | 35, 59 | impbid 211 |
1
β’ (π β ((SalGenβπ) = π β ((π β SAlg β§ βͺ π =
βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ
π¦ = βͺ π
β§ π β π¦) β π β π¦)))) |