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

Metamath Proof Explorer

Theorem chlejb1i

Description: Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ 𝐴 ∈ Cℋ
2 chjcl.2 ⊢ 𝐵 ∈ Cℋ
3 ssid ⊢ 𝐵 ⊆ 𝐵
4 1 2 2 chlubii ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐵 )
5 3 4 mpan2 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐵 )
6 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
7 5 6 jctir ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
8 eqss ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
9 7 8 sylibr ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 )
10 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
11 eqimss ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 → ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐵 )
12 10 11 sstrid ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 → 𝐴 ⊆ 𝐵 )
13 9 12 impbii ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∨ℋ 𝐵 ) = 𝐵 )