Theorem chsscon3

Description: Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chsscon3	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( 𝐴 ⊆ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ 𝐵 ) )
2		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) )
3	2	sseq2d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ) )
4	1 3	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ( 𝐴 ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ) ) )
5		sseq2	⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) )
6		fveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( ⊥ ‘ 𝐵 ) = ( ⊥ ‘ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) )
7	6	sseq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ↔ ( ⊥ ‘ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ) )
8	5 7	bibi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ↔ ( ⊥ ‘ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) ) ) )
9		ifchhv	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∈ Cℋ
10		ifchhv	⊢ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ∈ Cℋ
11	9 10	chsscon3i	⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ↔ ( ⊥ ‘ if ( 𝐵 ∈ Cℋ , 𝐵 , ℋ ) ) ⊆ ( ⊥ ‘ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ) )
12	4 8 11	dedth2h	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 ↔ ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )