Theorem oplecon3b

Description: Contraposition law for orthoposets. ( chsscon3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	opcon3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	opcon3.l	⊢ ≤ = ( le ‘ 𝐾 )
	opcon3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	oplecon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opcon3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		opcon3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		opcon3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4	1 2 3	oplecon3	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )
5		simp1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
6	1 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
7	6	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
8	1 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
9	8	3adant3	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
10	1 2 3	oplecon3	⊢ ( ( 𝐾 ∈ OP ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≤ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
11	5 7 9 10	syl3anc	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≤ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
12	1 3	opococ	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
13	12	3adant3	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
14	1 3	opococ	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
15	14	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
16	13 15	breq12d	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≤ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ↔ 𝑋 ≤ 𝑌 ) )
17	11 16	sylibd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) → 𝑋 ≤ 𝑌 ) )
18	4 17	impbid	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )