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

Metamath Proof Explorer

Theorem chrelati

Description: The Hilbert lattice is relatively atomic. Remark 2 of Kalmbach p. 149. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ 𝐴 ∈ Cℋ
chpssat.2 ⊢ 𝐵 ∈ Cℋ
Assertion chrelati ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ 𝐴 ∈ Cℋ
2 chpssat.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 chpssati ⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
4 ancom ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) )
5 pssss ⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 )
6 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
7 chnle ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) )
8 1 7 mpan ⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) )
9 8 adantl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) )
10 ibar ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) )
11 chlub ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
12 1 2 11 mp3an13 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
13 10 12 sylan9bb ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
14 9 13 anbi12d ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
15 5 6 14 syl2an ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ HAtoms ) → ( ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
16 4 15 bitrid ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
17 16 rexbidva ⊢ ( 𝐴 ⊊ 𝐵 → ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
18 3 17 mpbid ⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )