Step | Hyp | Ref
| Expression |
1 | | elfvdm 6880 |
. . . 4
β’ (π β (Unitβπ
) β π
β dom Unit) |
2 | | unit.1 |
. . . 4
β’ π = (Unitβπ
) |
3 | 1, 2 | eleq2s 2856 |
. . 3
β’ (π β π β π
β dom Unit) |
4 | 3 | elexd 3466 |
. 2
β’ (π β π β π
β V) |
5 | | df-br 5107 |
. . . 4
β’ (π β₯ 1 β β¨π, 1 β© β β₯
) |
6 | | elfvdm 6880 |
. . . . . 6
β’
(β¨π, 1 β© β
(β₯rβπ
) β π
β dom
β₯r) |
7 | | unit.3 |
. . . . . 6
β’ β₯ =
(β₯rβπ
) |
8 | 6, 7 | eleq2s 2856 |
. . . . 5
β’
(β¨π, 1 β© β
β₯
β π
β dom
β₯r) |
9 | 8 | elexd 3466 |
. . . 4
β’
(β¨π, 1 β© β
β₯
β π
β
V) |
10 | 5, 9 | sylbi 216 |
. . 3
β’ (π β₯ 1 β π
β V) |
11 | 10 | adantr 482 |
. 2
β’ ((π β₯ 1 β§ ππΈ 1 ) β π
β V) |
12 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π
β (β₯rβπ) =
(β₯rβπ
)) |
13 | 12, 7 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = π
β (β₯rβπ) = β₯ ) |
14 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π
β (opprβπ) =
(opprβπ
)) |
15 | | unit.4 |
. . . . . . . . . . . 12
β’ π =
(opprβπ
) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = π
β (opprβπ) = π) |
17 | 16 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π = π
β
(β₯rβ(opprβπ)) = (β₯rβπ)) |
18 | | unit.5 |
. . . . . . . . . 10
β’ πΈ =
(β₯rβπ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = π
β
(β₯rβ(opprβπ)) = πΈ) |
20 | 13, 19 | ineq12d 4174 |
. . . . . . . 8
β’ (π = π
β ((β₯rβπ) β©
(β₯rβ(opprβπ))) = ( β₯ β© πΈ)) |
21 | 20 | cnveqd 5832 |
. . . . . . 7
β’ (π = π
β β‘((β₯rβπ) β©
(β₯rβ(opprβπ))) = β‘( β₯ β© πΈ)) |
22 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π
β (1rβπ) = (1rβπ
)) |
23 | | unit.2 |
. . . . . . . . 9
β’ 1 =
(1rβπ
) |
24 | 22, 23 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = π
β (1rβπ) = 1 ) |
25 | 24 | sneqd 4599 |
. . . . . . 7
β’ (π = π
β {(1rβπ)} = { 1 }) |
26 | 21, 25 | imaeq12d 6015 |
. . . . . 6
β’ (π = π
β (β‘((β₯rβπ) β©
(β₯rβ(opprβπ))) β {(1rβπ)}) = (β‘( β₯ β© πΈ) β { 1 })) |
27 | | df-unit 20072 |
. . . . . 6
β’ Unit =
(π β V β¦ (β‘((β₯rβπ) β©
(β₯rβ(opprβπ))) β {(1rβπ)})) |
28 | 7 | fvexi 6857 |
. . . . . . . . 9
β’ β₯ β
V |
29 | 28 | inex1 5275 |
. . . . . . . 8
β’ ( β₯ β©
πΈ) β
V |
30 | 29 | cnvex 7863 |
. . . . . . 7
β’ β‘( β₯ β© πΈ) β V |
31 | 30 | imaex 7854 |
. . . . . 6
β’ (β‘( β₯ β© πΈ) β { 1 }) β
V |
32 | 26, 27, 31 | fvmpt 6949 |
. . . . 5
β’ (π
β V β
(Unitβπ
) = (β‘( β₯ β© πΈ) β { 1 })) |
33 | 2, 32 | eqtrid 2789 |
. . . 4
β’ (π
β V β π = (β‘( β₯ β© πΈ) β { 1 })) |
34 | 33 | eleq2d 2824 |
. . 3
β’ (π
β V β (π β π β π β (β‘( β₯ β© πΈ) β { 1 }))) |
35 | | inss1 4189 |
. . . . . 6
β’ ( β₯ β©
πΈ) β β₯ |
36 | 7 | reldvdsr 20074 |
. . . . . 6
β’ Rel β₯ |
37 | | relss 5738 |
. . . . . 6
β’ (( β₯ β©
πΈ) β β₯ β
(Rel β₯ β Rel ( β₯ β©
πΈ))) |
38 | 35, 36, 37 | mp2 9 |
. . . . 5
β’ Rel (
β₯
β© πΈ) |
39 | | eliniseg2 6059 |
. . . . 5
β’ (Rel (
β₯
β© πΈ) β (π β (β‘( β₯ β© πΈ) β { 1 }) β π( β₯ β© πΈ) 1 )) |
40 | 38, 39 | ax-mp 5 |
. . . 4
β’ (π β (β‘( β₯ β© πΈ) β { 1 }) β π( β₯ β© πΈ) 1 ) |
41 | | brin 5158 |
. . . 4
β’ (π( β₯ β© πΈ) 1 β (π β₯ 1 β§ ππΈ 1 )) |
42 | 40, 41 | bitri 275 |
. . 3
β’ (π β (β‘( β₯ β© πΈ) β { 1 }) β (π β₯ 1 β§ ππΈ 1 )) |
43 | 34, 42 | bitrdi 287 |
. 2
β’ (π
β V β (π β π β (π β₯ 1 β§ ππΈ 1 ))) |
44 | 4, 11, 43 | pm5.21nii 380 |
1
β’ (π β π β (π β₯ 1 β§ ππΈ 1 )) |