This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chnlei

Description: Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ⊢ 𝐴 ∈ Cℋ
chjcl.2 ⊢ 𝐵 ∈ Cℋ
Assertion chnlei ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ 𝐴 ∈ Cℋ
2 chjcl.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
4 3 biantrur ⊢ ( ¬ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) ) )
5 2 1 chlejb1i ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∨ℋ 𝐴 ) = 𝐴 )
6 eqcom ⊢ ( ( 𝐵 ∨ℋ 𝐴 ) = 𝐴 ↔ 𝐴 = ( 𝐵 ∨ℋ 𝐴 ) )
7 2 1 chjcomi ⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
8 7 eqeq2i ⊢ ( 𝐴 = ( 𝐵 ∨ℋ 𝐴 ) ↔ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) )
9 5 6 8 3bitri ⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) )
10 9 notbii ⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) )
11 dfpss2 ⊢ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 ∨ℋ 𝐵 ) ) )
12 4 10 11 3bitr4i ⊢ ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) )