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

Metamath Proof Explorer

Theorem chlejb1

Description: Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chlejb1 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B ↔ A ∨ ℋ B = B

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ⊆ B
2 oveq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∨ ℋ B
3 2 eqeq1d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∨ ℋ B = B ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = B
4 1 3 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⊆ B ↔ A ∨ ℋ B = B ↔ if A ∈ C ℋ A 0 ℋ ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = B
5 sseq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ⊆ if B ∈ C ℋ B 0 ℋ
6 oveq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∨ ℋ B = if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ
7 id ⊢ B = if B ∈ C ℋ B 0 ℋ → B = if B ∈ C ℋ B 0 ℋ
8 6 7 eqeq12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ∨ ℋ B = B ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if B ∈ C ℋ B 0 ℋ
9 5 8 bibi12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ B = B ↔ if A ∈ C ℋ A 0 ℋ ⊆ if B ∈ C ℋ B 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if B ∈ C ℋ B 0 ℋ
10 h0elch ⊢ 0 ℋ ∈ C ℋ
11 10 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
12 10 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
13 11 12 chlejb1i ⊢ if A ∈ C ℋ A 0 ℋ ⊆ if B ∈ C ℋ B 0 ℋ ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ if B ∈ C ℋ B 0 ℋ = if B ∈ C ℋ B 0 ℋ
14 4 9 13 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B ↔ A ∨ ℋ B = B