Step | Hyp | Ref
| Expression |
1 | | ipopos.i |
. . . . 5
β’ πΌ = (toIncβπΉ) |
2 | 1 | fvexi 6860 |
. . . 4
β’ πΌ β V |
3 | 2 | a1i 11 |
. . 3
β’ (πΉ β V β πΌ β V) |
4 | 1 | ipobas 18428 |
. . 3
β’ (πΉ β V β πΉ = (BaseβπΌ)) |
5 | | eqidd 2734 |
. . 3
β’ (πΉ β V β (leβπΌ) = (leβπΌ)) |
6 | | ssid 3970 |
. . . 4
β’ π β π |
7 | | eqid 2733 |
. . . . . 6
β’
(leβπΌ) =
(leβπΌ) |
8 | 1, 7 | ipole 18431 |
. . . . 5
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
9 | 8 | 3anidm23 1422 |
. . . 4
β’ ((πΉ β V β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
10 | 6, 9 | mpbiri 258 |
. . 3
β’ ((πΉ β V β§ π β πΉ) β π(leβπΌ)π) |
11 | 1, 7 | ipole 18431 |
. . . . 5
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
12 | 1, 7 | ipole 18431 |
. . . . . 6
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
13 | 12 | 3com23 1127 |
. . . . 5
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
14 | 11, 13 | anbi12d 632 |
. . . 4
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β ((π(leβπΌ)π β§ π(leβπΌ)π) β (π β π β§ π β π))) |
15 | | simpl 484 |
. . . . 5
β’ ((π β π β§ π β π) β π β π) |
16 | | simpr 486 |
. . . . 5
β’ ((π β π β§ π β π) β π β π) |
17 | 15, 16 | eqssd 3965 |
. . . 4
β’ ((π β π β§ π β π) β π = π) |
18 | 14, 17 | syl6bi 253 |
. . 3
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β ((π(leβπΌ)π β§ π(leβπΌ)π) β π = π)) |
19 | | sstr 3956 |
. . . . 5
β’ ((π β π β§ π β π) β π β π) |
20 | 19 | a1i 11 |
. . . 4
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β ((π β π β§ π β π) β π β π)) |
21 | 11 | 3adant3r3 1185 |
. . . . 5
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β (π(leβπΌ)π β π β π)) |
22 | 1, 7 | ipole 18431 |
. . . . . 6
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
23 | 22 | 3adant3r1 1183 |
. . . . 5
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β (π(leβπΌ)π β π β π)) |
24 | 21, 23 | anbi12d 632 |
. . . 4
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β ((π(leβπΌ)π β§ π(leβπΌ)π) β (π β π β§ π β π))) |
25 | 1, 7 | ipole 18431 |
. . . . 5
β’ ((πΉ β V β§ π β πΉ β§ π β πΉ) β (π(leβπΌ)π β π β π)) |
26 | 25 | 3adant3r2 1184 |
. . . 4
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β (π(leβπΌ)π β π β π)) |
27 | 20, 24, 26 | 3imtr4d 294 |
. . 3
β’ ((πΉ β V β§ (π β πΉ β§ π β πΉ β§ π β πΉ)) β ((π(leβπΌ)π β§ π(leβπΌ)π) β π(leβπΌ)π)) |
28 | 3, 4, 5, 10, 18, 27 | isposd 18220 |
. 2
β’ (πΉ β V β πΌ β Poset) |
29 | | fvprc 6838 |
. . . 4
β’ (Β¬
πΉ β V β
(toIncβπΉ) =
β
) |
30 | 1, 29 | eqtrid 2785 |
. . 3
β’ (Β¬
πΉ β V β πΌ = β
) |
31 | | 0pos 18218 |
. . 3
β’ β
β Poset |
32 | 30, 31 | eqeltrdi 2842 |
. 2
β’ (Β¬
πΉ β V β πΌ β Poset) |
33 | 28, 32 | pm2.61i 182 |
1
β’ πΌ β Poset |