Metamath Proof Explorer

Theorem elpcliN

Description: Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses elpcli.s 
|- S = ( PSubSp ` K )
elpcli.c 
|- U = ( PCl ` K )
Assertion elpcliN 
|- ( ( ( K e. V /\ X C_ Y /\ Y e. S ) /\ Q e. ( U ` X ) ) -> Q e. Y )

Proof

Step Hyp Ref Expression
1 elpcli.s 
 |-  S = ( PSubSp ` K )
2 elpcli.c 
 |-  U = ( PCl ` K )
3 simp1 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> K e. V )
4 simp2 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> X C_ Y )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 5 1 psubssat 
 |-  ( ( K e. V /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
7 6 3adant2 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
8 4 7 sstrd 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> X C_ ( Atoms ` K ) )
9 5 1 2 pclvalN 
 |-  ( ( K e. V /\ X C_ ( Atoms ` K ) ) -> ( U ` X ) = |^| { z e. S | X C_ z } )
10 3 8 9 syl2anc 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> ( U ` X ) = |^| { z e. S | X C_ z } )
11 10 eleq2d 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> ( Q e. ( U ` X ) <-> Q e. |^| { z e. S | X C_ z } ) )
12 elintrabg 
 |-  ( Q e. |^| { z e. S | X C_ z } -> ( Q e. |^| { z e. S | X C_ z } <-> A. z e. S ( X C_ z -> Q e. z ) ) )
13 12 ibi 
 |-  ( Q e. |^| { z e. S | X C_ z } -> A. z e. S ( X C_ z -> Q e. z ) )
14 11 13 biimtrdi 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> ( Q e. ( U ` X ) -> A. z e. S ( X C_ z -> Q e. z ) ) )
15 sseq2 
 |-  ( z = Y -> ( X C_ z <-> X C_ Y ) )
16 eleq2 
 |-  ( z = Y -> ( Q e. z <-> Q e. Y ) )
17 15 16 imbi12d 
 |-  ( z = Y -> ( ( X C_ z -> Q e. z ) <-> ( X C_ Y -> Q e. Y ) ) )
18 17 rspccv 
 |-  ( A. z e. S ( X C_ z -> Q e. z ) -> ( Y e. S -> ( X C_ Y -> Q e. Y ) ) )
19 18 com13 
 |-  ( X C_ Y -> ( Y e. S -> ( A. z e. S ( X C_ z -> Q e. z ) -> Q e. Y ) ) )
20 19 imp 
 |-  ( ( X C_ Y /\ Y e. S ) -> ( A. z e. S ( X C_ z -> Q e. z ) -> Q e. Y ) )
21 20 3adant1 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> ( A. z e. S ( X C_ z -> Q e. z ) -> Q e. Y ) )
22 14 21 syld 
 |-  ( ( K e. V /\ X C_ Y /\ Y e. S ) -> ( Q e. ( U ` X ) -> Q e. Y ) )
23 22 imp 
 |-  ( ( ( K e. V /\ X C_ Y /\ Y e. S ) /\ Q e. ( U ` X ) ) -> Q e. Y )