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

Metamath Proof Explorer

Theorem chnle

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

Ref Expression
Assertion chnle ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 sseq2 ⊢ A = if A ∈ C ℋ A 0 ℋ → B ⊆ A ↔ B ⊆ if A ∈ C ℋ A 0 ℋ
2 1 notbid ⊢ A = if A ∈ C ℋ A 0 ℋ → ¬ B ⊆ A ↔ ¬ B ⊆ if A ∈ C ℋ A 0 ℋ
3 id ⊢ A = if A ∈ C ℋ A 0 ℋ → A = if A ∈ C ℋ A 0 ℋ
4 oveq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∨ ℋ B
5 3 4 psseq12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⊂ A ∨ ℋ B ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ B
6 2 5 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B ↔ ¬ B ⊆ if A ∈ C ℋ A 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ B
7 sseq1 ⊢ B = if B ∈ C ℋ B 0 ℋ → B ⊆ if A ∈ C ℋ A 0 ℋ ↔ if B ∈ C ℋ B 0 ℋ ⊆ if A ∈ C ℋ A 0 ℋ
8 7 notbid ⊢ B = if B ∈ C ℋ B 0 ℋ → ¬ B ⊆ if A ∈ C ℋ A 0 ℋ ↔ ¬ if B ∈ C ℋ B 0 ℋ ⊆ if A ∈ C ℋ A 0 ℋ
9 oveq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
10 9 psseq2d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ B ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
11 8 10 bibi12d ⊢ B = if B ∈ C ℋ B 0 ℋ → ¬ B ⊆ if A ∈ C ℋ A 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ B ↔ ¬ if B ∈ C ℋ B 0 ℋ ⊆ if A ∈ C ℋ A 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
12 h0elch ⊢ 0 ℋ ∈ C ℋ
13 12 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
14 12 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
15 13 14 chnlei ⊢ ¬ if B ∈ C ℋ B 0 ℋ ⊆ if A ∈ C ℋ A 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ⊂ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
16 6 11 15 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B