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

Metamath Proof Explorer

Theorem 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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ∧ ( 𝑋 ∨ 𝑝 ) ≤ 𝑌 ) )