Step | Hyp | Ref
| Expression |
1 | | 2idlval.t |
. 2
β’ π = (2Idealβπ
) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π = π
β (LIdealβπ) = (LIdealβπ
)) |
3 | | 2idlval.i |
. . . . . 6
β’ πΌ = (LIdealβπ
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β (LIdealβπ) = πΌ) |
5 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π
β (opprβπ) =
(opprβπ
)) |
6 | | 2idlval.o |
. . . . . . . 8
β’ π =
(opprβπ
) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π
β (opprβπ) = π) |
8 | 7 | fveq2d 6847 |
. . . . . 6
β’ (π = π
β
(LIdealβ(opprβπ)) = (LIdealβπ)) |
9 | | 2idlval.j |
. . . . . 6
β’ π½ = (LIdealβπ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . 5
β’ (π = π
β
(LIdealβ(opprβπ)) = π½) |
11 | 4, 10 | ineq12d 4174 |
. . . 4
β’ (π = π
β ((LIdealβπ) β©
(LIdealβ(opprβπ))) = (πΌ β© π½)) |
12 | | df-2idl 20718 |
. . . 4
β’ 2Ideal =
(π β V β¦
((LIdealβπ) β©
(LIdealβ(opprβπ)))) |
13 | 3 | fvexi 6857 |
. . . . 5
β’ πΌ β V |
14 | 13 | inex1 5275 |
. . . 4
β’ (πΌ β© π½) β V |
15 | 11, 12, 14 | fvmpt 6949 |
. . 3
β’ (π
β V β
(2Idealβπ
) = (πΌ β© π½)) |
16 | | fvprc 6835 |
. . . 4
β’ (Β¬
π
β V β
(2Idealβπ
) =
β
) |
17 | | inss1 4189 |
. . . . 5
β’ (πΌ β© π½) β πΌ |
18 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
π
β V β
(LIdealβπ
) =
β
) |
19 | 3, 18 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π
β V β πΌ = β
) |
20 | | sseq0 4360 |
. . . . 5
β’ (((πΌ β© π½) β πΌ β§ πΌ = β
) β (πΌ β© π½) = β
) |
21 | 17, 19, 20 | sylancr 588 |
. . . 4
β’ (Β¬
π
β V β (πΌ β© π½) = β
) |
22 | 16, 21 | eqtr4d 2776 |
. . 3
β’ (Β¬
π
β V β
(2Idealβπ
) = (πΌ β© π½)) |
23 | 15, 22 | pm2.61i 182 |
. 2
β’
(2Idealβπ
) =
(πΌ β© π½) |
24 | 1, 23 | eqtri 2761 |
1
β’ π = (πΌ β© π½) |