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	3	simprbi	⊢ ( 𝐴 ⊊ 𝐵 → ¬ 𝐵 ⊆ 𝐴 )
5		iman	⊢ ( ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) ↔ ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
7		ss2rab	⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
8		ssrab2	⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ HAtoms
9		atssch	⊢ HAtoms ⊆ Cℋ
10	8 9	sstri	⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ Cℋ
11		ssrab2	⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ HAtoms
12	11 9	sstri	⊢ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ
13		chsupss	⊢ ( ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ Cℋ ∧ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ ) → ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) ) )
14	10 12 13	mp2an	⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ) ⊆ ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } ) )
15	2	hatomistici	⊢ 𝐵 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } )
16	1	hatomistici	⊢ 𝐴 = ( ∨ℋ ‘ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } )
17	14 15 16	3sstr4g	⊢ ( { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐵 } ⊆ { 𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴 } → 𝐵 ⊆ 𝐴 )
18	7 17	sylbir	⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
19	6 18	sylbir	⊢ ( ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
20	19	con3i	⊢ ( ¬ 𝐵 ⊆ 𝐴 → ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
21		dfrex2	⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
22	20 21	sylibr	⊢ ( ¬ 𝐵 ⊆ 𝐴 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )
23	4 22	syl	⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) )