Theorem opltcon3b

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

	Ref	Expression
Hypotheses	opltcon3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	opltcon3.s	⊢ < = ( lt ‘ 𝐾 )
	opltcon3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	opltcon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( ⊥ ‘ 𝑌 ) < ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opltcon3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		opltcon3.s	⊢ < = ( lt ‘ 𝐾 )
3		opltcon3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5	1 4 3	oplecon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) )
6	1 4 3	oplecon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ( le ‘ 𝐾 ) 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) )
7	6	3com23	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ( le ‘ 𝐾 ) 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) )
8	7	notbid	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ( le ‘ 𝐾 ) 𝑋 ↔ ¬ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) )
9	5 8	anbi12d	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( ( ⊥ ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) ) )
10		opposet	⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
11	1 4 2	pltval3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ) )
12	10 11	syl3an1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ ¬ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ) )
13	10	3ad2ant1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Poset )
14	1 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
15	14	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
16	1 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
17	16	3adant3	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
18	1 4 2	pltval3	⊢ ( ( 𝐾 ∈ Poset ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) < ( ⊥ ‘ 𝑋 ) ↔ ( ( ⊥ ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) ) )
19	13 15 17 18	syl3anc	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) < ( ⊥ ‘ 𝑋 ) ↔ ( ( ⊥ ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ( ⊥ ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑌 ) ) ) )
20	9 12 19	3bitr4d	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( ⊥ ‘ 𝑌 ) < ( ⊥ ‘ 𝑋 ) ) )