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

Theorem pclclN 34562
 Description: Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
pclfval.a
pclfval.s
pclfval.c
Assertion
Ref Expression
pclclN

Proof of Theorem pclclN
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pclfval.a . . 3
2 pclfval.s . . 3
3 pclfval.c . . 3
41, 2, 3pclvalN 34561 . 2
51, 2atpsubN 34424 . . . 4
6 sseq2 3519 . . . . 5
76intminss 4301 . . . 4
85, 7sylan 471 . . 3
9 r19.26 2982 . . . . . . . 8
10 jcab 859 . . . . . . . . 9
1110ralbii 2888 . . . . . . . 8
12 vex 3109 . . . . . . . . . 10
1312elintrab 4287 . . . . . . . . 9
14 vex 3109 . . . . . . . . . 10
1514elintrab 4287 . . . . . . . . 9
1613, 15anbi12i 697 . . . . . . . 8
179, 11, 163bitr4ri 278 . . . . . . 7
18 simpll1 1030 . . . . . . . . . . . . . 14
19 simplr 754 . . . . . . . . . . . . . 14
20 simpll3 1032 . . . . . . . . . . . . . 14
21 simprl 755 . . . . . . . . . . . . . 14
22 simprr 756 . . . . . . . . . . . . . 14
23 simpll2 1031 . . . . . . . . . . . . . 14
24 eqid 2460 . . . . . . . . . . . . . . 15
25 eqid 2460 . . . . . . . . . . . . . . 15
2624, 25, 1, 2psubspi2N 34419 . . . . . . . . . . . . . 14
2718, 19, 20, 21, 22, 23, 26syl33anc 1238 . . . . . . . . . . . . 13
2827ex 434 . . . . . . . . . . . 12
2928imim2d 52 . . . . . . . . . . 11
3029ralimdva 2865 . . . . . . . . . 10
31 vex 3109 . . . . . . . . . . 11
3231elintrab 4287 . . . . . . . . . 10
3330, 32syl6ibr 227 . . . . . . . . 9
34333exp 1190 . . . . . . . 8
3534com24 87 . . . . . . 7
3617, 35syl5bi 217 . . . . . 6
3736ralrimdv 2873 . . . . 5
3837ralrimivv 2877 . . . 4