Metamath Proof Explorer

Theorem pclclN

Description: Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a 
|- A = ( Atoms ` K )
pclfval.s 
|- S = ( PSubSp ` K )
pclfval.c 
|- U = ( PCl ` K )
Assertion pclclN 
|- ( ( K e. V /\ X C_ A ) -> ( U ` X ) e. S )

Proof

Step Hyp Ref Expression
1 pclfval.a 
 |-  A = ( Atoms ` K )
2 pclfval.s 
 |-  S = ( PSubSp ` K )
3 pclfval.c 
 |-  U = ( PCl ` K )
4 1 2 3 pclvalN 
 |-  ( ( K e. V /\ X C_ A ) -> ( U ` X ) = |^| { y e. S | X C_ y } )
5 1 2 atpsubN 
 |-  ( K e. V -> A e. S )
6 sseq2 
 |-  ( y = A -> ( X C_ y <-> X C_ A ) )
7 6 intminss 
 |-  ( ( A e. S /\ X C_ A ) -> |^| { y e. S | X C_ y } C_ A )
8 5 7 sylan 
 |-  ( ( K e. V /\ X C_ A ) -> |^| { y e. S | X C_ y } C_ A )
9 r19.26 
 |-  ( A. y e. S ( ( X C_ y -> p e. y ) /\ ( X C_ y -> q e. y ) ) <-> ( A. y e. S ( X C_ y -> p e. y ) /\ A. y e. S ( X C_ y -> q e. y ) ) )
10 jcab 
 |-  ( ( X C_ y -> ( p e. y /\ q e. y ) ) <-> ( ( X C_ y -> p e. y ) /\ ( X C_ y -> q e. y ) ) )
11 10 ralbii 
 |-  ( A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) <-> A. y e. S ( ( X C_ y -> p e. y ) /\ ( X C_ y -> q e. y ) ) )
12 vex 
 |-  p e. _V
13 12 elintrab 
 |-  ( p e. |^| { y e. S | X C_ y } <-> A. y e. S ( X C_ y -> p e. y ) )
14 vex 
 |-  q e. _V
15 14 elintrab 
 |-  ( q e. |^| { y e. S | X C_ y } <-> A. y e. S ( X C_ y -> q e. y ) )
16 13 15 anbi12i 
 |-  ( ( p e. |^| { y e. S | X C_ y } /\ q e. |^| { y e. S | X C_ y } ) <-> ( A. y e. S ( X C_ y -> p e. y ) /\ A. y e. S ( X C_ y -> q e. y ) ) )
17 9 11 16 3bitr4ri 
 |-  ( ( p e. |^| { y e. S | X C_ y } /\ q e. |^| { y e. S | X C_ y } ) <-> A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) )
18 simpll1 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> K e. V )
19 simplr 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> y e. S )
20 simpll3 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> r e. A )
21 simprl 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> p e. y )
22 simprr 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> q e. y )
23 simpll2 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> r ( le ` K ) ( p ( join ` K ) q ) )
24 eqid 
 |-  ( le ` K ) = ( le ` K )
25 eqid 
 |-  ( join ` K ) = ( join ` K )
26 24 25 1 2 psubspi2N 
 |-  ( ( ( K e. V /\ y e. S /\ r e. A ) /\ ( p e. y /\ q e. y /\ r ( le ` K ) ( p ( join ` K ) q ) ) ) -> r e. y )
27 18 19 20 21 22 23 26 syl33anc 
 |-  ( ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) /\ ( p e. y /\ q e. y ) ) -> r e. y )
28 27 ex 
 |-  ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) -> ( ( p e. y /\ q e. y ) -> r e. y ) )
29 28 imim2d 
 |-  ( ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) /\ y e. S ) -> ( ( X C_ y -> ( p e. y /\ q e. y ) ) -> ( X C_ y -> r e. y ) ) )
30 29 ralimdva 
 |-  ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) -> ( A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) -> A. y e. S ( X C_ y -> r e. y ) ) )
31 vex 
 |-  r e. _V
32 31 elintrab 
 |-  ( r e. |^| { y e. S | X C_ y } <-> A. y e. S ( X C_ y -> r e. y ) )
33 30 32 syl6ibr 
 |-  ( ( K e. V /\ r ( le ` K ) ( p ( join ` K ) q ) /\ r e. A ) -> ( A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) -> r e. |^| { y e. S | X C_ y } ) )
34 33 3exp 
 |-  ( K e. V -> ( r ( le ` K ) ( p ( join ` K ) q ) -> ( r e. A -> ( A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) -> r e. |^| { y e. S | X C_ y } ) ) ) )
35 34 com24 
 |-  ( K e. V -> ( A. y e. S ( X C_ y -> ( p e. y /\ q e. y ) ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) ) ) )
36 17 35 syl5bi 
 |-  ( K e. V -> ( ( p e. |^| { y e. S | X C_ y } /\ q e. |^| { y e. S | X C_ y } ) -> ( r e. A -> ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) ) ) )
37 36 ralrimdv 
 |-  ( K e. V -> ( ( p e. |^| { y e. S | X C_ y } /\ q e. |^| { y e. S | X C_ y } ) -> A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) ) )
38 37 ralrimivv 
 |-  ( K e. V -> A. p e. |^| { y e. S | X C_ y } A. q e. |^| { y e. S | X C_ y } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) )
39 38 adantr 
 |-  ( ( K e. V /\ X C_ A ) -> A. p e. |^| { y e. S | X C_ y } A. q e. |^| { y e. S | X C_ y } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) )
40 24 25 1 2 ispsubsp 
 |-  ( K e. V -> ( |^| { y e. S | X C_ y } e. S <-> ( |^| { y e. S | X C_ y } C_ A /\ A. p e. |^| { y e. S | X C_ y } A. q e. |^| { y e. S | X C_ y } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) ) ) )
41 40 adantr 
 |-  ( ( K e. V /\ X C_ A ) -> ( |^| { y e. S | X C_ y } e. S <-> ( |^| { y e. S | X C_ y } C_ A /\ A. p e. |^| { y e. S | X C_ y } A. q e. |^| { y e. S | X C_ y } A. r e. A ( r ( le ` K ) ( p ( join ` K ) q ) -> r e. |^| { y e. S | X C_ y } ) ) ) )
42 8 39 41 mpbir2and 
 |-  ( ( K e. V /\ X C_ A ) -> |^| { y e. S | X C_ y } e. S )
43 4 42 eqeltrd 
 |-  ( ( K e. V /\ X C_ A ) -> ( U ` X ) e. S )