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

Metamath Proof Explorer

Theorem occon3

Description: Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014) (New usage is discouraged.)

Ref Expression
Assertion occon3 ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ↔ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ococss ⊢ ( 𝐵 ⊆ ℋ → 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
2 1 adantl ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
3 ocss ⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) ⊆ ℋ )
4 occon ⊢ ( ( 𝐴 ⊆ ℋ ∧ ( ⊥ ‘ 𝐵 ) ⊆ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
5 3 4 sylan2 ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
6 sstr2 ⊢ ( 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ⊆ ( ⊥ ‘ 𝐴 ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )
7 2 5 6 sylsyld ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )
8 ococss ⊢ ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
9 8 adantr ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
10 id ⊢ ( 𝐵 ⊆ ℋ → 𝐵 ⊆ ℋ )
11 ocss ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
12 occon ⊢ ( ( 𝐵 ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
13 10 11 12 syl2anr ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐵 ) ) )
14 sstr2 ⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐵 ) → 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) )
15 9 13 14 sylsyld ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) → 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) )
16 7 15 impbid ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ↔ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) )