Theorem lplnbase 39280

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

Hypotheses

Ref	Expression
lplnbase.b	⊢ 𝐵 = (Base‘𝐾)
lplnbase.p	⊢ 𝑃 = (LPlanes‘𝐾)

Assertion

Ref	Expression
lplnbase	⊢ (𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵)

Proof of Theorem lplnbase

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  ∃wrex 3063  Vcvv 3472  ∅c0 4335   class class class wbr 5156  ‘cfv 6558  Basecbs 17234   ⋖ ccvr 39007  LLinesclln 39237  LPlanesclpl 39238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-iota 6510  df-fun 6560  df-fv 6566  df-lplanes 39245

This theorem is referenced by:  islpln2  39282  llnmlplnN  39285  lplnnle2at  39287  lplnneat  39291  lplnnelln  39292  llncvrlpln2  39303  2lplnmN  39305  lplncmp  39308  lplnexatN  39309  lplnexllnN  39310  2llnjaN  39312  islvol3  39322  lvoli3  39323  lvolnle3at  39328  lplncvrlvol2  39361  lplncvrlvol  39362  lvolcmp  39363  2lplnm2N  39367  2lplnmj  39368  dalemyeb  39395  dalem10  39419  dalem16  39425  dalem44  39462  dalem55  39473