Metamath Proof Explorer

Theorem llni

Description: Condition implying a lattice line. (Contributed by NM, 17-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 llni ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → X ∈ N

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 simpl2 ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → X ∈ B
6 breq1 ⊢ p = P → p C X ↔ P C X
7 6 rspcev ⊢ P ∈ A ∧ P C X → ∃ p ∈ A p C X
8 7 3ad2antl3 ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → ∃ p ∈ A p C X
9 simpl1 ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → K ∈ D
10 1 2 3 4 islln ⊢ K ∈ D → X ∈ N ↔ X ∈ B ∧ ∃ p ∈ A p C X
11 9 10 syl ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → X ∈ N ↔ X ∈ B ∧ ∃ p ∈ A p C X
12 5 8 11 mpbir2and ⊢ K ∈ D ∧ X ∈ B ∧ P ∈ A ∧ P C X → X ∈ N