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 syl5bb ( ( 𝐴𝐵𝑥 ∈ HAtoms ) → ( ( 𝑥𝐵 ∧ ¬ 𝑥𝐴 ) ↔ ( 𝐴 ⊊ ( 𝐴 𝑥 ) ∧ ( 𝐴 𝑥 ) ⊆ 𝐵 ) ) )
17 16 rexbidva ( 𝐴𝐵 → ( ∃ 𝑥 ∈ HAtoms ( 𝑥𝐵 ∧ ¬ 𝑥𝐴 ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 𝑥 ) ∧ ( 𝐴 𝑥 ) ⊆ 𝐵 ) ) )
18 3 17 mpbid ( 𝐴𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 𝑥 ) ∧ ( 𝐴 𝑥 ) ⊆ 𝐵 ) )