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

Metamath Proof Explorer

Theorem lplnbase

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

Ref Expression
Hypotheses lplnbase.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lplnbase.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnbase ( 𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 lplnbase.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lplnbase.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3 n0i ⊢ ( 𝑋 ∈ 𝑃 → ¬ 𝑃 = ∅ )
4 2 eqeq1i ⊢ ( 𝑃 = ∅ ↔ ( LPlanes ‘ 𝐾 ) = ∅ )
5 3 4 sylnib ⊢ ( 𝑋 ∈ 𝑃 → ¬ ( LPlanes ‘ 𝐾 ) = ∅ )
6 fvprc ⊢ ( ¬ 𝐾 ∈ V → ( LPlanes ‘ 𝐾 ) = ∅ )
7 5 6 nsyl2 ⊢ ( 𝑋 ∈ 𝑃 → 𝐾 ∈ V )
8 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
9 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
10 1 8 9 2 islpln ⊢ ( 𝐾 ∈ V → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑥 ∈ ( LLines ‘ 𝐾 ) 𝑥 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
11 10 simprbda ⊢ ( ( 𝐾 ∈ V ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ∈ 𝐵 )
12 7 11 mpancom ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵 )