Step | Hyp | Ref
| Expression |
1 | | trlset.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | trlset.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | trlset.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
4 | | trlset.m |
. . . 4
β’ β§ =
(meetβπΎ) |
5 | | trlset.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
6 | | trlset.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | | trlset.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
8 | | trlset.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | trlset 38627 |
. . 3
β’ ((πΎ β π β§ π β π») β π
= (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) |
10 | 9 | fveq1d 6845 |
. 2
β’ ((πΎ β π β§ π β π») β (π
βπΉ) = ((π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))βπΉ)) |
11 | | fveq1 6842 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
12 | 11 | oveq2d 7374 |
. . . . . . . 8
β’ (π = πΉ β (π β¨ (πβπ)) = (π β¨ (πΉβπ))) |
13 | 12 | oveq1d 7373 |
. . . . . . 7
β’ (π = πΉ β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) |
14 | 13 | eqeq2d 2748 |
. . . . . 6
β’ (π = πΉ β (π₯ = ((π β¨ (πβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
15 | 14 | imbi2d 341 |
. . . . 5
β’ (π = πΉ β ((Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)) β (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
16 | 15 | ralbidv 3175 |
. . . 4
β’ (π = πΉ β (βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)) β βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
17 | 16 | riotabidv 7316 |
. . 3
β’ (π = πΉ β (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
18 | | eqid 2737 |
. . 3
β’ (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) = (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) |
19 | | riotaex 7318 |
. . 3
β’
(β©π₯
β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π))) β V |
20 | 17, 18, 19 | fvmpt 6949 |
. 2
β’ (πΉ β π β ((π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))βπΉ) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
21 | 10, 20 | sylan9eq 2797 |
1
β’ (((πΎ β π β§ π β π») β§ πΉ β π) β (π
βπΉ) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |