Metamath Proof Explorer


Theorem chsscon1

Description: Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chsscon1 ( ( 𝐴C𝐵C ) → ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 choccl ( 𝐴C → ( ⊥ ‘ 𝐴 ) ∈ C )
2 chsscon3 ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝐵C ) → ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
3 1 2 sylan ( ( 𝐴C𝐵C ) → ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) )
4 ococ ( 𝐴C → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴 )
5 4 adantr ( ( 𝐴C𝐵C ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴 )
6 5 sseq2d ( ( 𝐴C𝐵C ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) )
7 3 6 bitrd ( ( 𝐴C𝐵C ) → ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) )