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 | chsscon1i | ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ch0le.1 | ⊢ 𝐴 ∈ Cℋ | |
2 | chjcl.2 | ⊢ 𝐵 ∈ Cℋ | |
3 | 1 | choccli | ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ |
4 | 3 2 | chsscon3i | ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ) |
5 | 1 | pjococi | ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴 |
6 | 5 | sseq2i | ⊢ ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) |
7 | 4 6 | bitri | ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) |