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

Metamath Proof Explorer

Theorem chpssati

Description: Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ 𝐴 ∈ Cℋ
2 chpssat.2 ⊢ 𝐵 ∈ Cℋ
3 dfpss3 ⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) )
4 iman ⊢ ( ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) ↔ ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
5 4 ralbii ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
6 ss2rab ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
7 ssrab2 ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ HAtoms
8 atssch ⊢ HAtoms ⊆ Cℋ
9 7 8 sstri ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ Cℋ
10 ssrab2 ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ HAtoms
11 10 8 sstri ⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ
12 chsupss ⊢ ( ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ Cℋ ∧ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ ) → ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
13 9 11 12 mp2an ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
14 2 hatomistici ⊢ 𝐵 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } )
15 1 hatomistici ⊢ 𝐴 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
16 13 14 15 3sstr4g ⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → 𝐵 ⊆ 𝐴 )
17 6 16 sylbir ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
18 5 17 sylbir ⊢ ( ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
19 18 con3i ⊢ ( ¬ 𝐵 ⊆ 𝐴 → ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
20 dfrex2 ⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
21 19 20 sylibr ⊢ ( ¬ 𝐵 ⊆ 𝐴 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
22 3 21 simplbiim ⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )