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 ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )