Metamath Proof Explorer


Theorem llnbase

Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012)

Ref Expression
Hypotheses llnbase.b 𝐵 = ( Base ‘ 𝐾 )
llnbase.n 𝑁 = ( LLines ‘ 𝐾 )
Assertion llnbase ( 𝑋𝑁𝑋𝐵 )

Proof

Step Hyp Ref Expression
1 llnbase.b 𝐵 = ( Base ‘ 𝐾 )
2 llnbase.n 𝑁 = ( LLines ‘ 𝐾 )
3 n0i ( 𝑋𝑁 → ¬ 𝑁 = ∅ )
4 2 eqeq1i ( 𝑁 = ∅ ↔ ( LLines ‘ 𝐾 ) = ∅ )
5 3 4 sylnib ( 𝑋𝑁 → ¬ ( LLines ‘ 𝐾 ) = ∅ )
6 fvprc ( ¬ 𝐾 ∈ V → ( LLines ‘ 𝐾 ) = ∅ )
7 5 6 nsyl2 ( 𝑋𝑁𝐾 ∈ V )
8 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
9 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 1 8 9 2 islln ( 𝐾 ∈ V → ( 𝑋𝑁 ↔ ( 𝑋𝐵 ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
11 10 simprbda ( ( 𝐾 ∈ V ∧ 𝑋𝑁 ) → 𝑋𝐵 )
12 7 11 mpancom ( 𝑋𝑁𝑋𝐵 )