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 ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) )