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

Metamath Proof Explorer

Theorem chsscon3i

Description: Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ⊢ 𝐴 ∈ Cℋ
chjcl.2 ⊢ 𝐵 ∈ Cℋ
Assertion chsscon3i ( 𝐴 ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ 𝐴 ∈ Cℋ
2 chjcl.2 ⊢ 𝐵 ∈ Cℋ
3 1 chssii ⊢ 𝐴 ⊆ ℋ
4 2 chssii ⊢ 𝐵 ⊆ ℋ
5 occon ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
6 3 4 5 mp2an ⊢ ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) )
7 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
8 7 chssii ⊢ ( ⊥ ‘ 𝐵 ) ⊆ ℋ
9 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
10 9 chssii ⊢ ( ⊥ ‘ 𝐴 ) ⊆ ℋ
11 occon ⊢ ( ( ( ⊥ ‘ 𝐵 ) ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
12 8 10 11 mp2an ⊢ ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
13 1 pjococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
14 2 pjococi ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵
15 12 13 14 3sstr3g ⊢ ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) → 𝐴 ⊆ 𝐵 )
16 6 15 impbii ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) )