Theorem opcon1b

Description: Orthocomplement contraposition law. ( negcon1 analog.) (Contributed by NM, 24-Jan-2012)

	Ref	Expression
Hypotheses	opoccl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	opoccl.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	opcon1b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) = 𝑌 ↔ ( ⊥ ‘ 𝑌 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		opoccl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		opoccl.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3	1 2	opcon2b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ⊥ ‘ 𝑌 ) ↔ 𝑌 = ( ⊥ ‘ 𝑋 ) ) )
4		eqcom	⊢ ( ( ⊥ ‘ 𝑌 ) = 𝑋 ↔ 𝑋 = ( ⊥ ‘ 𝑌 ) )
5		eqcom	⊢ ( ( ⊥ ‘ 𝑋 ) = 𝑌 ↔ 𝑌 = ( ⊥ ‘ 𝑋 ) )
6	3 4 5	3bitr4g	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) = 𝑌 ) )
7	6	bicomd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) = 𝑌 ↔ ( ⊥ ‘ 𝑌 ) = 𝑋 ) )