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