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