Step | Hyp | Ref
| Expression |
1 | | hlop 38232 |
. . . . 5
β’ (πΎ β HL β πΎ β OP) |
2 | | pmapglb2.g |
. . . . . . . 8
β’ πΊ = (glbβπΎ) |
3 | | eqid 2733 |
. . . . . . . 8
β’
(1.βπΎ) =
(1.βπΎ) |
4 | 2, 3 | glb0N 38063 |
. . . . . . 7
β’ (πΎ β OP β (πΊββ
) =
(1.βπΎ)) |
5 | 4 | fveq2d 6896 |
. . . . . 6
β’ (πΎ β OP β (πβ(πΊββ
)) = (πβ(1.βπΎ))) |
6 | | pmapglb2.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
7 | | pmapglb2.m |
. . . . . . 7
β’ π = (pmapβπΎ) |
8 | 3, 6, 7 | pmap1N 38638 |
. . . . . 6
β’ (πΎ β OP β (πβ(1.βπΎ)) = π΄) |
9 | 5, 8 | eqtrd 2773 |
. . . . 5
β’ (πΎ β OP β (πβ(πΊββ
)) = π΄) |
10 | 1, 9 | syl 17 |
. . . 4
β’ (πΎ β HL β (πβ(πΊββ
)) = π΄) |
11 | | rexeq 3322 |
. . . . . . . . 9
β’ (πΌ = β
β (βπ β πΌ π¦ = π β βπ β β
π¦ = π)) |
12 | 11 | abbidv 2802 |
. . . . . . . 8
β’ (πΌ = β
β {π¦ β£ βπ β πΌ π¦ = π} = {π¦ β£ βπ β β
π¦ = π}) |
13 | | rex0 4358 |
. . . . . . . . 9
β’ Β¬
βπ β β
π¦ = π |
14 | 13 | abf 4403 |
. . . . . . . 8
β’ {π¦ β£ βπ β β
π¦ = π} = β
|
15 | 12, 14 | eqtrdi 2789 |
. . . . . . 7
β’ (πΌ = β
β {π¦ β£ βπ β πΌ π¦ = π} = β
) |
16 | 15 | fveq2d 6896 |
. . . . . 6
β’ (πΌ = β
β (πΊβ{π¦ β£ βπ β πΌ π¦ = π}) = (πΊββ
)) |
17 | 16 | fveq2d 6896 |
. . . . 5
β’ (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (πβ(πΊββ
))) |
18 | | riin0 5086 |
. . . . 5
β’ (πΌ = β
β (π΄ β© β© π β πΌ (πβπ)) = π΄) |
19 | 17, 18 | eqeq12d 2749 |
. . . 4
β’ (πΌ = β
β ((πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)) β (πβ(πΊββ
)) = π΄)) |
20 | 10, 19 | syl5ibrcom 246 |
. . 3
β’ (πΎ β HL β (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
21 | 20 | adantr 482 |
. 2
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ = β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
22 | | pmapglb2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
23 | 22, 2, 7 | pmapglbx 38640 |
. . . 4
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = β©
π β πΌ (πβπ)) |
24 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π πΎ β HL |
25 | | nfra1 3282 |
. . . . . . . . . 10
β’
β²πβπ β πΌ π β π΅ |
26 | 24, 25 | nfan 1903 |
. . . . . . . . 9
β’
β²π(πΎ β HL β§ βπ β πΌ π β π΅) |
27 | | simpr 486 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β π β πΌ) |
28 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β πΎ β HL) |
29 | | rspa 3246 |
. . . . . . . . . . . . 13
β’
((βπ β
πΌ π β π΅ β§ π β πΌ) β π β π΅) |
30 | 29 | adantll 713 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β π β π΅) |
31 | 22, 6, 7 | pmapssat 38630 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β π΄) |
32 | 28, 30, 31 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β (πβπ) β π΄) |
33 | 27, 32 | jca 513 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ βπ β πΌ π β π΅) β§ π β πΌ) β (π β πΌ β§ (πβπ) β π΄)) |
34 | 33 | ex 414 |
. . . . . . . . 9
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (π β πΌ β (π β πΌ β§ (πβπ) β π΄))) |
35 | 26, 34 | eximd 2210 |
. . . . . . . 8
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (βπ π β πΌ β βπ(π β πΌ β§ (πβπ) β π΄))) |
36 | | n0 4347 |
. . . . . . . 8
β’ (πΌ β β
β
βπ π β πΌ) |
37 | | df-rex 3072 |
. . . . . . . 8
β’
(βπ β
πΌ (πβπ) β π΄ β βπ(π β πΌ β§ (πβπ) β π΄)) |
38 | 35, 36, 37 | 3imtr4g 296 |
. . . . . . 7
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ β β
β βπ β πΌ (πβπ) β π΄)) |
39 | 38 | 3impia 1118 |
. . . . . 6
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β βπ β πΌ (πβπ) β π΄) |
40 | | iinss 5060 |
. . . . . 6
β’
(βπ β
πΌ (πβπ) β π΄ β β©
π β πΌ (πβπ) β π΄) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β β© π β πΌ (πβπ) β π΄) |
42 | | sseqin2 4216 |
. . . . 5
β’ (β© π β πΌ (πβπ) β π΄ β (π΄ β© β©
π β πΌ (πβπ)) = β©
π β πΌ (πβπ)) |
43 | 41, 42 | sylib 217 |
. . . 4
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (π΄ β© β©
π β πΌ (πβπ)) = β©
π β πΌ (πβπ)) |
44 | 23, 43 | eqtr4d 2776 |
. . 3
β’ ((πΎ β HL β§ βπ β πΌ π β π΅ β§ πΌ β β
) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ))) |
45 | 44 | 3expia 1122 |
. 2
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πΌ β β
β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ)))) |
46 | 21, 45 | pm2.61dne 3029 |
1
β’ ((πΎ β HL β§ βπ β πΌ π β π΅) β (πβ(πΊβ{π¦ β£ βπ β πΌ π¦ = π})) = (π΄ β© β©
π β πΌ (πβπ))) |