Step |
Hyp |
Ref |
Expression |
1 |
|
pleval2.b |
|- B = ( Base ` K ) |
2 |
|
pleval2.l |
|- .<_ = ( le ` K ) |
3 |
|
pleval2.s |
|- .< = ( lt ` K ) |
4 |
|
elfvdm |
|- ( X e. ( Base ` K ) -> K e. dom Base ) |
5 |
4 1
|
eleq2s |
|- ( X e. B -> K e. dom Base ) |
6 |
5
|
adantr |
|- ( ( X e. B /\ Y e. B ) -> K e. dom Base ) |
7 |
2 3
|
pltval |
|- ( ( K e. dom Base /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) ) |
8 |
7
|
3expb |
|- ( ( K e. dom Base /\ ( X e. B /\ Y e. B ) ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) ) |
9 |
6 8
|
mpancom |
|- ( ( X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) ) |
10 |
9
|
biimpar |
|- ( ( ( X e. B /\ Y e. B ) /\ ( X .<_ Y /\ X =/= Y ) ) -> X .< Y ) |
11 |
10
|
expr |
|- ( ( ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X =/= Y -> X .< Y ) ) |
12 |
11
|
necon1bd |
|- ( ( ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( -. X .< Y -> X = Y ) ) |
13 |
12
|
orrd |
|- ( ( ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( X .< Y \/ X = Y ) ) |
14 |
13
|
ex |
|- ( ( X e. B /\ Y e. B ) -> ( X .<_ Y -> ( X .< Y \/ X = Y ) ) ) |