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

Theorem pclfinN 33434
 Description: The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 33484. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
pclfin.a
pclfin.c
Assertion
Ref Expression
pclfinN
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem pclfinN
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 458 . . 3
2 elin 3649 . . . . . . . 8
3 elpwi 3990 . . . . . . . . 9
43adantl 467 . . . . . . . 8
52, 4sylbi 198 . . . . . . 7
6 simpll 758 . . . . . . . . 9
7 sstr 3472 . . . . . . . . . . . 12
87ancoms 454 . . . . . . . . . . 11
98adantll 718 . . . . . . . . . 10
10 pclfin.a . . . . . . . . . . 11
11 eqid 2422 . . . . . . . . . . 11
12 pclfin.c . . . . . . . . . . 11
1310, 11, 12pclclN 33425 . . . . . . . . . 10
146, 9, 13syl2anc 665 . . . . . . . . 9
1510, 11psubssat 33288 . . . . . . . . 9
166, 14, 15syl2anc 665 . . . . . . . 8
1716ex 435 . . . . . . 7
185, 17syl5 33 . . . . . 6
1918ralrimiv 2834 . . . . 5
20 iunss 4340 . . . . 5
2119, 20sylibr 215 . . . 4
22 eliun 4304 . . . . . . . . 9
23 fveq2 5881 . . . . . . . . . . 11
2423eleq2d 2492 . . . . . . . . . 10
2524cbvrexv 3055 . . . . . . . . 9
2622, 25bitri 252 . . . . . . . 8
27 eliun 4304 . . . . . . . . 9
28 fveq2 5881 . . . . . . . . . . 11
2928eleq2d 2492 . . . . . . . . . 10
3029cbvrexv 3055 . . . . . . . . 9
3127, 30bitri 252 . . . . . . . 8
3226, 31anbi12i 701 . . . . . . 7
33 elin 3649 . . . . . . . . . . 11
34 elpwi 3990 . . . . . . . . . . . 12
3534anim2i 571 . . . . . . . . . . 11
3633, 35sylbi 198 . . . . . . . . . 10
37 elin 3649 . . . . . . . . . . . . . 14
38 elpwi 3990 . . . . . . . . . . . . . . 15
3938anim2i 571 . . . . . . . . . . . . . 14
4037, 39sylbi 198 . . . . . . . . . . . . 13
41 simp2rl 1074 . . . . . . . . . . . . . . . . . . . 20
42 simp12l 1118 . . . . . . . . . . . . . . . . . . . 20
43 unfi 7847 . . . . . . . . . . . . . . . . . . . 20
4441, 42, 43syl2anc 665 . . . . . . . . . . . . . . . . . . 19
45 simp2rr 1075 . . . . . . . . . . . . . . . . . . . . 21
46 simp12r 1119 . . . . . . . . . . . . . . . . . . . . 21
4745, 46unssd 3642 . . . . . . . . . . . . . . . . . . . 20
48 vex 3083 . . . . . . . . . . . . . . . . . . . . . 22
49 vex 3083 . . . . . . . . . . . . . . . . . . . . . 22
5048, 49unex 6603 . . . . . . . . . . . . . . . . . . . . 21
5150elpw 3987 . . . . . . . . . . . . . . . . . . . 20
5247, 51sylibr 215 . . . . . . . . . . . . . . . . . . 19
5344, 52elind 3650 . . . . . . . . . . . . . . . . . 18
54 simp11l 1116 . . . . . . . . . . . . . . . . . . 19
55 simp11r 1117 . . . . . . . . . . . . . . . . . . . . . 22
5645, 55sstrd 3474 . . . . . . . . . . . . . . . . . . . . 21
5746, 55sstrd 3474 . . . . . . . . . . . . . . . . . . . . 21
5856, 57unssd 3642 . . . . . . . . . . . . . . . . . . . 20
5910, 11, 12pclclN 33425 . . . . . . . . . . . . . . . . . . . 20
6054, 58, 59syl2anc 665 . . . . . . . . . . . . . . . . . . 19
61 simp3l 1033 . . . . . . . . . . . . . . . . . . 19
62 ssun1 3629 . . . . . . . . . . . . . . . . . . . . . 22
6362a1i 11 . . . . . . . . . . . . . . . . . . . . 21
6410, 12pclssN 33428 . . . . . . . . . . . . . . . . . . . . 21
6554, 63, 58, 64syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20
66 simp2l 1031 . . . . . . . . . . . . . . . . . . . 20
6765, 66sseldd 3465 . . . . . . . . . . . . . . . . . . 19
68 ssun2 3630 . . . . . . . . . . . . . . . . . . . . . 22
6968a1i 11 . . . . . . . . . . . . . . . . . . . . 21
7010, 12pclssN 33428 . . . . . . . . . . . . . . . . . . . . 21
7154, 69, 58, 70syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20
72 simp13 1037 . . . . . . . . . . . . . . . . . . . 20
7371, 72sseldd 3465 . . . . . . . . . . . . . . . . . . 19
74 simp3r 1034 . . . . . . . . . . . . . . . . . . 19
75 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
76 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
7775, 76, 10, 11psubspi2N 33282 . . . . . . . . . . . . . . . . . . 19
7854, 60, 61, 67, 73, 74, 77syl33anc 1279 . . . . . . . . . . . . . . . . . 18
79 fveq2 5881 . . . . . . . . . . . . . . . . . . . 20
8079eleq2d 2492 . . . . . . . . . . . . . . . . . . 19
8180rspcev 3182 . . . . . . . . . . . . . . . . . 18
8253, 78, 81syl2anc 665 . . . . . . . . . . . . . . . . 17
83 eliun 4304 . . . . . . . . . . . . . . . . 17
8482, 83sylibr 215 . . . . . . . . . . . . . . . 16
85843exp 1204 . . . . . . . . . . . . . . 15
8685exp5c 619 . . . . . . . . . . . . . 14
87863exp 1204 . . . . . . . . . . . . 13
8840, 87syl5 33 . . . . . . . . . . . 12
8988rexlimdv 2912 . . . . . . . . . . 11
9089com24 90 . . . . . . . . . 10
9136, 90syl5 33 . . . . . . . . 9
9291rexlimdv 2912 . . . . . . . 8
9392impd 432 . . . . . . 7
9432, 93syl5bi 220 . . . . . 6
9594ralrimdv 2838 . . . . 5
9695ralrimivv 2842 . . . 4
9775, 76, 10, 11ispsubsp 33279 . . . . 5
9897adantr 466 . . . 4
9921, 96, 98mpbir2and 930 . . 3
100 snfi 7660 . . . . . . . . 9
101100a1i 11 . . . . . . . 8
102 snelpwi 4666 . . . . . . . . 9
103102adantl 467 . . . . . . . 8
104101, 103elind 3650 . . . . . . 7
105 ssnid 4027 . . . . . . . 8
106 simpll 758 . . . . . . . . 9
107 ssel2 3459 . . . . . . . . . . 11
108107adantll 718 . . . . . . . . . 10
10910, 11snatpsubN 33284 . . . . . . . . . 10
110106, 108, 109syl2anc 665 . . . . . . . . 9
11111, 12pclidN 33430 . . . . . . . . 9
112106, 110, 111syl2anc 665 . . . . . . . 8
113105, 112syl5eleqr 2514 . . . . . . 7
114 fveq2 5881 . . . . . . . . 9
115114eleq2d 2492 . . . . . . . 8
116115rspcev 3182 . . . . . . 7
117104, 113, 116syl2anc 665 . . . . . 6
118117ex 435 . . . . 5
119 eliun 4304 . . . . 5
120118, 119syl6ibr 230 . . . 4
121120ssrdv 3470 . . 3
122 simpr 462 . . . . . . . . . 10
123 simplr 760 . . . . . . . . . 10
12410, 12pclssN 33428 . . . . . . . . . 10
1256, 122, 123, 124syl3anc 1264 . . . . . . . . 9
126125sseld 3463 . . . . . . . 8
127126ex 435 . . . . . . 7
1285, 127syl5 33 . . . . . 6
129128rexlimdv 2912 . . . . 5
130119, 129syl5bi 220 . . . 4
131130ssrdv 3470 . . 3
13211, 12pclbtwnN 33431 . . 3
1331, 99, 121, 131, 132syl22anc 1265 . 2
134133eqcomd 2430 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2771  wrex 2772   cun 3434   cin 3435   wss 3436  cpw 3981  csn 3998  ciun 4299   class class class wbr 4423  cfv 5601  (class class class)co 6305  cfn 7580  cple 15196  cjn 16188  catm 32798  cal 32799  cpsubsp 33030  cpclN 33421 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-oadd 7197  df-er 7374  df-en 7581  df-fin 7584  df-preset 16172  df-poset 16190  df-plt 16203  df-lub 16219  df-glb 16220  df-join 16221  df-meet 16222  df-p0 16284  df-lat 16291  df-covers 32801  df-ats 32802  df-atl 32833  df-psubsp 33037  df-pclN 33422 This theorem is referenced by:  pclcmpatN  33435
 Copyright terms: Public domain W3C validator