Step | Hyp | Ref
| Expression |
1 | | trlset.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
2 | | trlset.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | trlset.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | trlset.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
5 | | trlset.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
6 | | trlset.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
7 | | trlset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
8 | 2, 3, 4, 5, 6, 7 | trlfset 39031 |
. . . 4
β’ (πΎ β πΆ β (trLβπΎ) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))) |
9 | 8 | fveq1d 6894 |
. . 3
β’ (πΎ β πΆ β ((trLβπΎ)βπ) = ((π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))βπ)) |
10 | 1, 9 | eqtrid 2785 |
. 2
β’ (πΎ β πΆ β π
= ((π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))βπ)) |
11 | | fveq2 6892 |
. . . . 5
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
12 | | breq2 5153 |
. . . . . . . . 9
β’ (π€ = π β (π β€ π€ β π β€ π)) |
13 | 12 | notbid 318 |
. . . . . . . 8
β’ (π€ = π β (Β¬ π β€ π€ β Β¬ π β€ π)) |
14 | | oveq2 7417 |
. . . . . . . . 9
β’ (π€ = π β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π)) |
15 | 14 | eqeq2d 2744 |
. . . . . . . 8
β’ (π€ = π β (π₯ = ((π β¨ (πβπ)) β§ π€) β π₯ = ((π β¨ (πβπ)) β§ π))) |
16 | 13, 15 | imbi12d 345 |
. . . . . . 7
β’ (π€ = π β ((Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)) β (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) |
17 | 16 | ralbidv 3178 |
. . . . . 6
β’ (π€ = π β (βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)) β βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) |
18 | 17 | riotabidv 7367 |
. . . . 5
β’ (π€ = π β (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€))) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) |
19 | 11, 18 | mpteq12dv 5240 |
. . . 4
β’ (π€ = π β (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))) = (π β ((LTrnβπΎ)βπ) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) |
20 | | eqid 2733 |
. . . 4
β’ (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€))))) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€))))) |
21 | | fvex 6905 |
. . . . 5
β’
((LTrnβπΎ)βπ) β V |
22 | 21 | mptex 7225 |
. . . 4
β’ (π β ((LTrnβπΎ)βπ) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) β V |
23 | 19, 20, 22 | fvmpt 6999 |
. . 3
β’ (π β π» β ((π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))βπ) = (π β ((LTrnβπΎ)βπ) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) |
24 | | trlset.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
25 | 24 | mpteq1i 5245 |
. . 3
β’ (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) = (π β ((LTrnβπΎ)βπ) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π)))) |
26 | 23, 25 | eqtr4di 2791 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))βπ) = (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) |
27 | 10, 26 | sylan9eq 2793 |
1
β’ ((πΎ β πΆ β§ π β π») β π
= (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) |