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ℋ ) → ( ( ⊥ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ 𝐴 ) ) |