Step | Hyp | Ref
| Expression |
1 | | inass 4184 |
. . . . 5
β’ ((π΄ β© πΎ) β© βͺ π½) = (π΄ β© (πΎ β© βͺ π½)) |
2 | | in32 4186 |
. . . . 5
β’ ((π΄ β© πΎ) β© βͺ π½) = ((π΄ β© βͺ π½) β© πΎ) |
3 | 1, 2 | eqtr3i 2767 |
. . . 4
β’ (π΄ β© (πΎ β© βͺ π½)) = ((π΄ β© βͺ π½) β© πΎ) |
4 | | df-kgen 22901 |
. . . . . . . . . . 11
β’
πGen = (π
β Top β¦ {π₯
β π« βͺ π β£ βπ¦ β π« βͺ π((π βΎt π¦) β Comp β (π₯ β© π¦) β (π βΎt π¦))}) |
5 | 4 | mptrcl 6962 |
. . . . . . . . . 10
β’ (π΄ β
(πGenβπ½)
β π½ β
Top) |
6 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β π½
β Top) |
7 | | toptopon2 22283 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
8 | 6, 7 | sylib 217 |
. . . . . . . 8
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β π½
β (TopOnββͺ π½)) |
9 | | simpl 484 |
. . . . . . . 8
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β π΄
β (πGenβπ½)) |
10 | | elkgen 22903 |
. . . . . . . . 9
β’ (π½ β (TopOnββͺ π½)
β (π΄ β
(πGenβπ½)
β (π΄ β βͺ π½
β§ βπ¦ β
π« βͺ π½((π½ βΎt π¦) β Comp β (π΄ β© π¦) β (π½ βΎt π¦))))) |
11 | 10 | biimpa 478 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ π΄ β
(πGenβπ½))
β (π΄ β βͺ π½
β§ βπ¦ β
π« βͺ π½((π½ βΎt π¦) β Comp β (π΄ β© π¦) β (π½ βΎt π¦)))) |
12 | 8, 9, 11 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β βͺ π½ β§ βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β (π΄ β© π¦) β (π½ βΎt π¦)))) |
13 | 12 | simpld 496 |
. . . . . 6
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β π΄
β βͺ π½) |
14 | | df-ss 3932 |
. . . . . 6
β’ (π΄ β βͺ π½
β (π΄ β© βͺ π½) =
π΄) |
15 | 13, 14 | sylib 217 |
. . . . 5
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β© βͺ π½) = π΄) |
16 | 15 | ineq1d 4176 |
. . . 4
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β ((π΄
β© βͺ π½) β© πΎ) = (π΄ β© πΎ)) |
17 | 3, 16 | eqtrid 2789 |
. . 3
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β© (πΎ β© βͺ π½))
= (π΄ β© πΎ)) |
18 | | cmptop 22762 |
. . . . . . . 8
β’ ((π½ βΎt πΎ) β Comp β (π½ βΎt πΎ) β Top) |
19 | 18 | adantl 483 |
. . . . . . 7
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β Top) |
20 | | restrcl 22524 |
. . . . . . . 8
β’ ((π½ βΎt πΎ) β Top β (π½ β V β§ πΎ β V)) |
21 | 20 | simprd 497 |
. . . . . . 7
β’ ((π½ βΎt πΎ) β Top β πΎ β V) |
22 | 19, 21 | syl 17 |
. . . . . 6
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β πΎ
β V) |
23 | | eqid 2737 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
24 | 23 | restin 22533 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β V) β (π½ βΎt πΎ) = (π½ βΎt (πΎ β© βͺ π½))) |
25 | 6, 22, 24 | syl2anc 585 |
. . . . 5
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π½
βΎt πΎ) =
(π½ βΎt
(πΎ β© βͺ π½))) |
26 | | simpr 486 |
. . . . 5
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π½
βΎt πΎ)
β Comp) |
27 | 25, 26 | eqeltrrd 2839 |
. . . 4
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π½
βΎt (πΎ
β© βͺ π½)) β Comp) |
28 | | oveq2 7370 |
. . . . . . 7
β’ (π¦ = (πΎ β© βͺ π½) β (π½ βΎt π¦) = (π½ βΎt (πΎ β© βͺ π½))) |
29 | 28 | eleq1d 2823 |
. . . . . 6
β’ (π¦ = (πΎ β© βͺ π½) β ((π½ βΎt π¦) β Comp β (π½ βΎt (πΎ β© βͺ π½)) β
Comp)) |
30 | | ineq2 4171 |
. . . . . . 7
β’ (π¦ = (πΎ β© βͺ π½) β (π΄ β© π¦) = (π΄ β© (πΎ β© βͺ π½))) |
31 | 30, 28 | eleq12d 2832 |
. . . . . 6
β’ (π¦ = (πΎ β© βͺ π½) β ((π΄ β© π¦) β (π½ βΎt π¦) β (π΄ β© (πΎ β© βͺ π½)) β (π½ βΎt (πΎ β© βͺ π½)))) |
32 | 29, 31 | imbi12d 345 |
. . . . 5
β’ (π¦ = (πΎ β© βͺ π½) β (((π½ βΎt π¦) β Comp β (π΄ β© π¦) β (π½ βΎt π¦)) β ((π½ βΎt (πΎ β© βͺ π½)) β Comp β (π΄ β© (πΎ β© βͺ π½)) β (π½ βΎt (πΎ β© βͺ π½))))) |
33 | 12 | simprd 497 |
. . . . 5
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β βπ¦ β π« βͺ π½((π½ βΎt π¦) β Comp β (π΄ β© π¦) β (π½ βΎt π¦))) |
34 | | inss2 4194 |
. . . . . 6
β’ (πΎ β© βͺ π½)
β βͺ π½ |
35 | | inex1g 5281 |
. . . . . . 7
β’ (πΎ β V β (πΎ β© βͺ π½)
β V) |
36 | | elpwg 4568 |
. . . . . . 7
β’ ((πΎ β© βͺ π½)
β V β ((πΎ β©
βͺ π½) β π« βͺ π½
β (πΎ β© βͺ π½)
β βͺ π½)) |
37 | 22, 35, 36 | 3syl 18 |
. . . . . 6
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β ((πΎ
β© βͺ π½) β π« βͺ π½
β (πΎ β© βͺ π½)
β βͺ π½)) |
38 | 34, 37 | mpbiri 258 |
. . . . 5
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (πΎ
β© βͺ π½) β π« βͺ π½) |
39 | 32, 33, 38 | rspcdva 3585 |
. . . 4
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β ((π½
βΎt (πΎ
β© βͺ π½)) β Comp β (π΄ β© (πΎ β© βͺ π½)) β (π½ βΎt (πΎ β© βͺ π½)))) |
40 | 27, 39 | mpd 15 |
. . 3
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β© (πΎ β© βͺ π½))
β (π½
βΎt (πΎ
β© βͺ π½))) |
41 | 17, 40 | eqeltrrd 2839 |
. 2
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β© πΎ) β (π½ βΎt (πΎ β© βͺ π½))) |
42 | 41, 25 | eleqtrrd 2841 |
1
β’ ((π΄ β
(πGenβπ½)
β§ (π½
βΎt πΎ)
β Comp) β (π΄
β© πΎ) β (π½ βΎt πΎ)) |