This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ≤ ( ⊥ ‘ 𝑋 ) ) )