hlrelat3

Description: The Hilbert lattice is relatively atomic. Stronger version of hlrelat . (Contributed by NM, 2-May-2012)

	Ref	Expression
Hypotheses	hlrelat3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlrelat3.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlrelat3.s	⊢ < = ( lt ‘ 𝐾 )
	hlrelat3.j	⊢ ∨ = ( join ‘ 𝐾 )
	hlrelat3.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	hlrelat3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlrelat3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		hlrelat3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		hlrelat3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		hlrelat3.s	⊢ < = ( lt ‘ 𝐾 )
4		hlrelat3.j	⊢ ∨ = ( join ‘ 𝐾 )
5		hlrelat3.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6		hlrelat3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7	1 2 3 6	hlrelat1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
8	7	imp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) )
9		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ¬ 𝑝 ≤ 𝑋 )
10		simp1l1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝐾 ∈ HL )
11		simp1l2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
12		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑝 ∈ 𝐴 )
13	1 2 4 5 6	cvr1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑝 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
14	10 11 12 13	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ( ¬ 𝑝 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
15	9 14	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) )
16		simp1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
17		simp1r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑋 < 𝑌 )
18	2 3	pltle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
19	16 17 18	sylc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑋 ≤ 𝑌 )
20		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑝 ≤ 𝑌 )
21	10	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝐾 ∈ Lat )
22	1 6	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
23	12 22	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑝 ∈ 𝐵 )
24		simp1l3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
25	1 2 4	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑝 ≤ 𝑌 ) ↔ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )
26	21 11 23 24 25	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑝 ≤ 𝑌 ) ↔ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )
27	19 20 26	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 )
28	15 27	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )
29	28	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( 𝑝 ∈ 𝐴 → ( ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) ) )
30	29	reximdvai	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) ) )
31	8 30	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )

Metamath Proof Explorer

Theorem hlrelat3

Proof