Metamath Proof Explorer


Theorem opltcon3b

Description: Contraposition law for strict ordering in orthoposets. ( chpsscon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses opltcon3.b B = Base K
opltcon3.s < ˙ = < K
opltcon3.o ˙ = oc K
Assertion opltcon3b K OP X B Y B X < ˙ Y ˙ Y < ˙ ˙ X

Proof

Step Hyp Ref Expression
1 opltcon3.b B = Base K
2 opltcon3.s < ˙ = < K
3 opltcon3.o ˙ = oc K
4 eqid K = K
5 1 4 3 oplecon3b K OP X B Y B X K Y ˙ Y K ˙ X
6 1 4 3 oplecon3b K OP Y B X B Y K X ˙ X K ˙ Y
7 6 3com23 K OP X B Y B Y K X ˙ X K ˙ Y
8 7 notbid K OP X B Y B ¬ Y K X ¬ ˙ X K ˙ Y
9 5 8 anbi12d K OP X B Y B X K Y ¬ Y K X ˙ Y K ˙ X ¬ ˙ X K ˙ Y
10 opposet K OP K Poset
11 1 4 2 pltval3 K Poset X B Y B X < ˙ Y X K Y ¬ Y K X
12 10 11 syl3an1 K OP X B Y B X < ˙ Y X K Y ¬ Y K X
13 10 3ad2ant1 K OP X B Y B K Poset
14 1 3 opoccl K OP Y B ˙ Y B
15 14 3adant2 K OP X B Y B ˙ Y B
16 1 3 opoccl K OP X B ˙ X B
17 16 3adant3 K OP X B Y B ˙ X B
18 1 4 2 pltval3 K Poset ˙ Y B ˙ X B ˙ Y < ˙ ˙ X ˙ Y K ˙ X ¬ ˙ X K ˙ Y
19 13 15 17 18 syl3anc K OP X B Y B ˙ Y < ˙ ˙ X ˙ Y K ˙ X ¬ ˙ X K ˙ Y
20 9 12 19 3bitr4d K OP X B Y B X < ˙ Y ˙ Y < ˙ ˙ X