Theorem opcon2b

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

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

Proof

Step	Hyp	Ref	Expression
1		opoccl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		opoccl.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3	1 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
4	3	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
5	1 2	opcon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 = ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ 𝑋 ) ) )
6	4 5	syld3an3	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ 𝑋 ) ) )
7	1 2	opococ	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
8	7	3adant2	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
9	8	eqeq1d	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ 𝑋 ) ↔ 𝑌 = ( ⊥ ‘ 𝑋 ) ) )
10	6 9	bitrd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( ⊥ ‘ 𝑌 ) ↔ 𝑌 = ( ⊥ ‘ 𝑋 ) ) )