Theorem occon2

Description: Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	occon2	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ocss	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
2		ocss	⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) ⊆ ℋ )
3	1 2	anim12ci	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) )
4		occon	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )
5		occon	⊢ ( ( ( ⊥ ‘ 𝐵 ) ⊆ ℋ ∧ ( ⊥ ‘ 𝐴 ) ⊆ ℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
6	3 4 5	sylsyld	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )