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

Metamath Proof Explorer

Theorem llnset

Description: The set of lattice lines in a Hilbert lattice. (Contributed by NM, 16-Jun-2012)

Ref Expression
Hypotheses llnset.b ⊢ B = Base K
llnset.c ⊢ C = ⋖ K
llnset.a ⊢ A = Atoms ⁡ K
llnset.n ⊢ N = LLines ⁡ K
Assertion llnset ⊢ K ∈ D → N = x ∈ B | ∃ p ∈ A p C x

Proof

Step Hyp Ref Expression
1 llnset.b ⊢ B = Base K
2 llnset.c ⊢ C = ⋖ K
3 llnset.a ⊢ A = Atoms ⁡ K
4 llnset.n ⊢ N = LLines ⁡ K
5 elex ⊢ K ∈ D → K ∈ V
6 fveq2 ⊢ k = K → Base k = Base K
7 6 1 eqtr4di ⊢ k = K → Base k = B
8 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
9 8 3 eqtr4di ⊢ k = K → Atoms ⁡ k = A
10 fveq2 ⊢ k = K → ⋖ k = ⋖ K
11 10 2 eqtr4di ⊢ k = K → ⋖ k = C
12 11 breqd ⊢ k = K → p ⋖ k x ↔ p C x
13 9 12 rexeqbidv ⊢ k = K → ∃ p ∈ Atoms ⁡ k p ⋖ k x ↔ ∃ p ∈ A p C x
14 7 13 rabeqbidv ⊢ k = K → x ∈ Base k | ∃ p ∈ Atoms ⁡ k p ⋖ k x = x ∈ B | ∃ p ∈ A p C x
15 df-llines ⊢ LLines = k ∈ V ⟼ x ∈ Base k | ∃ p ∈ Atoms ⁡ k p ⋖ k x
16 1 fvexi ⊢ B ∈ V
17 16 rabex ⊢ x ∈ B | ∃ p ∈ A p C x ∈ V
18 14 15 17 fvmpt ⊢ K ∈ V → LLines ⁡ K = x ∈ B | ∃ p ∈ A p C x
19 4 18 eqtrid ⊢ K ∈ V → N = x ∈ B | ∃ p ∈ A p C x
20 5 19 syl ⊢ K ∈ D → N = x ∈ B | ∃ p ∈ A p C x