Step | Hyp | Ref
| Expression |
1 | | ltrnset.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
2 | | ltrnset.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | ltrnset.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
4 | | ltrnset.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
5 | | ltrnset.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
6 | | ltrnset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
7 | 2, 3, 4, 5, 6 | ltrnfset 38630 |
. . . 4
β’ (πΎ β π΅ β (LTrnβπΎ) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})) |
8 | 7 | fveq1d 6848 |
. . 3
β’ (πΎ β π΅ β ((LTrnβπΎ)βπ) = ((π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})βπ)) |
9 | 1, 8 | eqtrid 2785 |
. 2
β’ (πΎ β π΅ β π = ((π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})βπ)) |
10 | | fveq2 6846 |
. . . . 5
β’ (π€ = π β ((LDilβπΎ)βπ€) = ((LDilβπΎ)βπ)) |
11 | | ltrnset.d |
. . . . 5
β’ π· = ((LDilβπΎ)βπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . 4
β’ (π€ = π β ((LDilβπΎ)βπ€) = π·) |
13 | | breq2 5113 |
. . . . . . . 8
β’ (π€ = π β (π β€ π€ β π β€ π)) |
14 | 13 | notbid 318 |
. . . . . . 7
β’ (π€ = π β (Β¬ π β€ π€ β Β¬ π β€ π)) |
15 | | breq2 5113 |
. . . . . . . 8
β’ (π€ = π β (π β€ π€ β π β€ π)) |
16 | 15 | notbid 318 |
. . . . . . 7
β’ (π€ = π β (Β¬ π β€ π€ β Β¬ π β€ π)) |
17 | 14, 16 | anbi12d 632 |
. . . . . 6
β’ (π€ = π β ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β (Β¬ π β€ π β§ Β¬ π β€ π))) |
18 | | oveq2 7369 |
. . . . . . 7
β’ (π€ = π β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π)) |
19 | | oveq2 7369 |
. . . . . . 7
β’ (π€ = π β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π)) |
20 | 18, 19 | eqeq12d 2749 |
. . . . . 6
β’ (π€ = π β (((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))) |
21 | 17, 20 | imbi12d 345 |
. . . . 5
β’ (π€ = π β (((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€)) β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π)))) |
22 | 21 | 2ralbidv 3209 |
. . . 4
β’ (π€ = π β (βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π)))) |
23 | 12, 22 | rabeqbidv 3423 |
. . 3
β’ (π€ = π β {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))} = {π β π· β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))}) |
24 | | eqid 2733 |
. . 3
β’ (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))}) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))}) |
25 | 11 | fvexi 6860 |
. . . 4
β’ π· β V |
26 | 25 | rabex 5293 |
. . 3
β’ {π β π· β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))} β V |
27 | 23, 24, 26 | fvmpt 6952 |
. 2
β’ (π β π» β ((π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})βπ) = {π β π· β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))}) |
28 | 9, 27 | sylan9eq 2793 |
1
β’ ((πΎ β π΅ β§ π β π») β π = {π β π· β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))}) |