Theorem islpoldN 35064

Description: Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
lpolset.v	|- V = ( Base ` W )
lpolset.s	|- S = ( LSubSp ` W )
lpolset.z	|- .0. = ( 0g ` W )
lpolset.a	|- A = (LSAtoms ` W )
lpolset.h	|- H = (LSHyp ` W )
lpolset.p	|- P = (LPol ` W )
islpold.w	|- ( ph -> W e. X )
islpold.1	|- ( ph -> ._|_ : ~P V --> S )
islpold.2	|- ( ph -> ( ._|_ ` V ) = { .0. } )
islpold.3	|- ( ( ph /\ ( x C_ V /\ y C_ V /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
islpold.4	|- ( ( ph /\ x e. A ) -> ( ._|_ ` x ) e. H )
islpold.5	|- ( ( ph /\ x e. A ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )

Assertion

Ref	Expression
islpoldN	|- ( ph -> ._|_ e. P )

Distinct variable groups:   x, A   x, y, W   x, ._|_ , y   ph, x, y

Allowed substitution hints:   A( y)   P( x, y)   S( x, y)   H( x, y)   V( x, y)   X( x, y)   .0. ( x, y)

Proof of Theorem islpoldN

Step	Hyp	Ref	Expression
1		islpold.1	. 2 |- ( ph -> ._|_ : ~P V --> S )
2		islpold.2	. . 3 |- ( ph -> ( ._|_ ` V ) = { .0. } )
3		islpold.3	. . . . 5 |- ( ( ph /\ ( x C_ V /\ y C_ V /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
4	3	ex 436	. . . 4 |- ( ph -> ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
5	4	alrimivv 1776	. . 3 |- ( ph -> A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) )
6		islpold.4	. . . . 5 |- ( ( ph /\ x e. A ) -> ( ._|_ ` x ) e. H )
7		islpold.5	. . . . 5 |- ( ( ph /\ x e. A ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )
8	6, 7	jca 535	. . . 4 |- ( ( ph /\ x e. A ) -> ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
9	8	ralrimiva 2804	. . 3 |- ( ph -> A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) )
10	2, 5, 9	3jca 1189	. 2 |- ( ph -> ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) )
11		islpold.w	. . 3 |- ( ph -> W e. X )
12		lpolset.v	. . . 4 |- V = ( Base ` W )
13		lpolset.s	. . . 4 |- S = ( LSubSp ` W )
14		lpolset.z	. . . 4 |- .0. = ( 0g ` W )
15		lpolset.a	. . . 4 |- A = (LSAtoms ` W )
16		lpolset.h	. . . 4 |- H = (LSHyp ` W )
17		lpolset.p	. . . 4 |- P = (LPol ` W )
18	12, 13, 14, 15, 16, 17	islpolN 35063	. . 3 |- ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
19	11, 18	syl 17	. 2 |- ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { .0. } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. A ( ( ._|_ ` x ) e. H /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
20	1, 10, 19	mpbir2and 934	1 |- ( ph -> ._|_ e. P )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 986   A.wal 1444   = wceq 1446   e. wcel 1889   A.wral 2739   C_ wss 3406   ~Pcpw 3953   {csn 3970   -->wf 5581   ` cfv 5585   Basecbs 15133   0gc0g 15350   LSubSpclss 18167  LSAtomsclsa 32552  LSHypclsh 32553  LPolclpoN 35060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479  df-lpolN 35061

This theorem is referenced by:  dochpolN  35070