Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elpcliN Structured version   Unicode version

Theorem elpcliN 30690
 Description: Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
elpcli.s
elpcli.c
Assertion
Ref Expression
elpcliN

Proof of Theorem elpcliN
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp1 957 . . . . . 6
2 simp2 958 . . . . . . 7
3 eqid 2436 . . . . . . . . 9
4 elpcli.s . . . . . . . . 9
53, 4psubssat 30551 . . . . . . . 8
653adant2 976 . . . . . . 7
72, 6sstrd 3358 . . . . . 6
8 elpcli.c . . . . . . 7
93, 4, 8pclvalN 30687 . . . . . 6
101, 7, 9syl2anc 643 . . . . 5
1110eleq2d 2503 . . . 4
12 elintrabg 4063 . . . . 5
1312ibi 233 . . . 4
1411, 13syl6bi 220 . . 3
15 sseq2 3370 . . . . . . . 8
16 eleq2 2497 . . . . . . . 8
1715, 16imbi12d 312 . . . . . . 7
1817rspccv 3049 . . . . . 6
1918com13 76 . . . . 5
2019imp 419 . . . 4