Step | Hyp | Ref
| Expression |
1 | | hlop 38535 |
. . . . 5
β’ (πΎ β HL β πΎ β OP) |
2 | | pmapglb2.g |
. . . . . . . 8
β’ πΊ = (glbβπΎ) |
3 | | eqid 2730 |
. . . . . . . 8
β’
(1.βπΎ) =
(1.βπΎ) |
4 | 2, 3 | glb0N 38366 |
. . . . . . 7
β’ (πΎ β OP β (πΊββ
) =
(1.βπΎ)) |
5 | 4 | fveq2d 6894 |
. . . . . 6
β’ (πΎ β OP β (πβ(πΊββ
)) = (πβ(1.βπΎ))) |
6 | | pmapglb2.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
7 | | pmapglb2.m |
. . . . . . 7
β’ π = (pmapβπΎ) |
8 | 3, 6, 7 | pmap1N 38941 |
. . . . . 6
β’ (πΎ β OP β (πβ(1.βπΎ)) = π΄) |
9 | 5, 8 | eqtrd 2770 |
. . . . 5
β’ (πΎ β OP β (πβ(πΊββ
)) = π΄) |
10 | 1, 9 | syl 17 |
. . . 4
β’ (πΎ β HL β (πβ(πΊββ
)) = π΄) |
11 | | rexeq 3319 |
. . . . . . . . 9
β’ (πΌ = β
β (βπ β πΌ π¦ = π β βπ β β
π¦ = π)) |
12 | 11 | abbidv 2799 |
. . . . . . . 8
β’ (πΌ = β
β {π¦ β£ βπ β πΌ π¦ = π} = {π¦ β£ βπ β β
π¦ = π}) |
13 | | rex0 4356 |
. . . . . . . . 9
β’ Β¬
βπ β β
π¦ = π |
14 | 13 | abf 4401 |
. . . . . . . 8
β’ {π¦ β£ βπ β β
π¦ = π} = β
|
15 | 12, 14 | eqtrdi 2786 |
. . . . . . 7
β’ (πΌ = β
β {π¦ β£ βπ β πΌ π¦ = π} = β
) |
16 | 15 | fveq2d 6894 |
. . . . . 6
β’ (πΌ = β
β (πΊβ{π¦ β£ βπ β πΌ π¦ = π}) = (πΊββ
)) |
17 | 16 | fveq2d 6894 |
. . . . 5
β’ (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (πβ(πΊββ
))) |
18 | | riin0 5084 |
. . . . 5
β’ (πΌ = β
β (π΄ β© β© π β πΌ (πβπ)) = π΄) |
19 | 17, 18 | eqeq12d 2746 |
. . . 4
β’ (πΌ = β
β ((πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)) β (πβ(πΊββ
)) = π΄)) |
20 | 10, 19 | syl5ibrcom 246 |
. . 3
β’ (πΎ β HL β (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
21 | 20 | adantr 479 |
. 2
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
22 | | pmapglb2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
23 | 22, 2, 7 | pmapglbx 38943 |
. . . 4
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = β©
π β πΌ (πβπ)) |
24 | | nfv 1915 |
. . . . . . . . . 10
β’
β²π πΎ β HL |
25 | | nfra1 3279 |
. . . . . . . . . 10
β’
β²πβπ β πΌ π β π΅ |
26 | 24, 25 | nfan 1900 |
. . . . . . . . 9
β’
β²π(πΎ β HL β§ βπ β πΌ π β π΅) |
27 | | simpr 483 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β π β πΌ) |
28 | | simpll 763 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β πΎ β HL) |
29 | | rspa 3243 |
. . . . . . . . . . . . 13
β’
((βπ β
πΌ π β π΅ β§ π β πΌ) β π β π΅) |
30 | 29 | adantll 710 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β π β π΅) |
31 | 22, 6, 7 | pmapssat 38933 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β π΄) |
32 | 28, 30, 31 | syl2anc 582 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β (πβπ) β π΄) |
33 | 27, 32 | jca 510 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β (π β πΌ β§ (πβπ) β π΄)) |
34 | 33 | ex 411 |
. . . . . . . . 9
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (π β πΌ β (π β πΌ β§ (πβπ) β π΄))) |
35 | 26, 34 | eximd 2207 |
. . . . . . . 8
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (βπ π β πΌ β βπ(π β πΌ β§ (πβπ) β π΄))) |
36 | | n0 4345 |
. . . . . . . 8
β’ (πΌ β β
β
βπ π β πΌ) |
37 | | df-rex 3069 |
. . . . . . . 8
β’
(βπ β
πΌ (πβπ) β π΄ β βπ(π β πΌ β§ (πβπ) β π΄)) |
38 | 35, 36, 37 | 3imtr4g 295 |
. . . . . . 7
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ β β
β βπ β πΌ (πβπ) β π΄)) |
39 | 38 | 3impia 1115 |
. . . . . 6
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β βπ β πΌ (πβπ) β π΄) |
40 | | iinss 5058 |
. . . . . 6
β’
(βπ β
πΌ (πβπ) β π΄ β β©
π β πΌ (πβπ) β π΄) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β β© π β πΌ (πβπ) β π΄) |
42 | | sseqin2 4214 |
. . . . 5
β’ (β© π β πΌ (πβπ) β π΄ β (π΄ β© β©
π β πΌ (πβπ)) = β©
π β πΌ (πβπ)) |
43 | 41, 42 | sylib 217 |
. . . 4
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (π΄ β© β©
π β πΌ (πβπ)) = β©
π β πΌ (πβπ)) |
44 | 23, 43 | eqtr4d 2773 |
. . 3
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ))) |
45 | 44 | 3expia 1119 |
. 2
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ β β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
46 | 21, 45 | pm2.61dne 3026 |
1
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ))) |