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

Metamath Proof Explorer

Definition df-hlat

Description: Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012)

Ref Expression
Assertion df-hlat HL = { 𝑙 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlt ⊢ HL
1 vl ⊢ 𝑙
2 coml ⊢ OML
3 ccla ⊢ CLat
4 2 3 cin ⊢ ( OML ∩ CLat )
5 clc ⊢ CvLat
6 4 5 cin ⊢ ( ( OML ∩ CLat ) ∩ CvLat )
7 va ⊢ 𝑎
8 catm ⊢ Atoms
9 1 cv ⊢ 𝑙
10 9 8 cfv ⊢ ( Atoms ‘ 𝑙 )
11 vb ⊢ 𝑏
12 7 cv ⊢ 𝑎
13 11 cv ⊢ 𝑏
14 12 13 wne ⊢ 𝑎 ≠ 𝑏
15 vc ⊢ 𝑐
16 15 cv ⊢ 𝑐
17 16 12 wne ⊢ 𝑐 ≠ 𝑎
18 16 13 wne ⊢ 𝑐 ≠ 𝑏
19 cple ⊢ le
20 9 19 cfv ⊢ ( le ‘ 𝑙 )
21 cjn ⊢ join
22 9 21 cfv ⊢ ( join ‘ 𝑙 )
23 12 13 22 co ⊢ ( 𝑎 ( join ‘ 𝑙 ) 𝑏 )
24 16 23 20 wbr ⊢ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 )
25 17 18 24 w3a ⊢ ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) )
26 25 15 10 wrex ⊢ ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) )
27 14 26 wi ⊢ ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
28 27 11 10 wral ⊢ ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
29 28 7 10 wral ⊢ ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
30 cbs ⊢ Base
31 9 30 cfv ⊢ ( Base ‘ 𝑙 )
32 cp0 ⊢ 0.
33 9 32 cfv ⊢ ( 0. ‘ 𝑙 )
34 cplt ⊢ lt
35 9 34 cfv ⊢ ( lt ‘ 𝑙 )
36 33 12 35 wbr ⊢ ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎
37 12 13 35 wbr ⊢ 𝑎 ( lt ‘ 𝑙 ) 𝑏
38 36 37 wa ⊢ ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 )
39 13 16 35 wbr ⊢ 𝑏 ( lt ‘ 𝑙 ) 𝑐
40 cp1 ⊢ 1.
41 9 40 cfv ⊢ ( 1. ‘ 𝑙 )
42 16 41 35 wbr ⊢ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 )
43 39 42 wa ⊢ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) )
44 38 43 wa ⊢ ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
45 44 15 31 wrex ⊢ ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
46 45 11 31 wrex ⊢ ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
47 46 7 31 wrex ⊢ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
48 29 47 wa ⊢ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) )
49 48 1 6 crab ⊢ { 𝑙 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) ) }
50 0 49 wceq ⊢ HL = { 𝑙 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) ) }