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

Theorem pclfinN 30770
 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 30820. (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 445 . . 3
2 elin 3532 . . . . . . . 8
3 elpwi 3809 . . . . . . . . 9
43adantl 454 . . . . . . . 8
52, 4sylbi 189 . . . . . . 7
6 simpll 732 . . . . . . . . 9
7 sstr 3358 . . . . . . . . . . . 12
87ancoms 441 . . . . . . . . . . 11
98adantll 696 . . . . . . . . . 10
10 pclfin.a . . . . . . . . . . 11
11 eqid 2438 . . . . . . . . . . 11
12 pclfin.c . . . . . . . . . . 11
1310, 11, 12pclclN 30761 . . . . . . . . . 10
146, 9, 13syl2anc 644 . . . . . . . . 9
1510, 11psubssat 30624 . . . . . . . . 9
166, 14, 15syl2anc 644 . . . . . . . 8
1716ex 425 . . . . . . 7
185, 17syl5 31 . . . . . 6
1918ralrimiv 2790 . . . . 5
20 iunss 4134 . . . . 5
2119, 20sylibr 205 . . . 4
22 eliun 4099 . . . . . . . . 9
23 fveq2 5731 . . . . . . . . . . 11
2423eleq2d 2505 . . . . . . . . . 10
2524cbvrexv 2935 . . . . . . . . 9
2622, 25bitri 242 . . . . . . . 8
27 eliun 4099 . . . . . . . . 9
28 fveq2 5731 . . . . . . . . . . 11
2928eleq2d 2505 . . . . . . . . . 10
3029cbvrexv 2935 . . . . . . . . 9
3127, 30bitri 242 . . . . . . . 8
3226, 31anbi12i 680 . . . . . . 7
33 elin 3532 . . . . . . . . . . 11
34 elpwi 3809 . . . . . . . . . . . 12
3534anim2i 554 . . . . . . . . . . 11
3633, 35sylbi 189 . . . . . . . . . 10
37 elin 3532 . . . . . . . . . . . . . 14
38 elpwi 3809 . . . . . . . . . . . . . . 15
3938anim2i 554 . . . . . . . . . . . . . 14
4037, 39sylbi 189 . . . . . . . . . . . . 13
41 simp2rl 1027 . . . . . . . . . . . . . . . . . . . 20
42 simp12l 1071 . . . . . . . . . . . . . . . . . . . 20
43 unfi 7377 . . . . . . . . . . . . . . . . . . . 20
4441, 42, 43syl2anc 644 . . . . . . . . . . . . . . . . . . 19
45 simp2rr 1028 . . . . . . . . . . . . . . . . . . . . 21
46 simp12r 1072 . . . . . . . . . . . . . . . . . . . . 21
4745, 46unssd 3525 . . . . . . . . . . . . . . . . . . . 20
48 vex 2961 . . . . . . . . . . . . . . . . . . . . . 22
49 vex 2961 . . . . . . . . . . . . . . . . . . . . . 22
5048, 49unex 4710 . . . . . . . . . . . . . . . . . . . . 21
5150elpw 3807 . . . . . . . . . . . . . . . . . . . 20
5247, 51sylibr 205 . . . . . . . . . . . . . . . . . . 19
53 elin 3532 . . . . . . . . . . . . . . . . . . 19
5444, 52, 53sylanbrc 647 . . . . . . . . . . . . . . . . . 18
55 simp11l 1069 . . . . . . . . . . . . . . . . . . 19
56 simp11r 1070 . . . . . . . . . . . . . . . . . . . . . 22
5745, 56sstrd 3360 . . . . . . . . . . . . . . . . . . . . 21
5846, 56sstrd 3360 . . . . . . . . . . . . . . . . . . . . 21
5957, 58unssd 3525 . . . . . . . . . . . . . . . . . . . 20
6010, 11, 12pclclN 30761 . . . . . . . . . . . . . . . . . . . 20
6155, 59, 60syl2anc 644 . . . . . . . . . . . . . . . . . . 19
62 simp3l 986 . . . . . . . . . . . . . . . . . . 19
63 ssun1 3512 . . . . . . . . . . . . . . . . . . . . . 22
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21
6510, 12pclssN 30764 . . . . . . . . . . . . . . . . . . . . 21
6655, 64, 59, 65syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20
67 simp2l 984 . . . . . . . . . . . . . . . . . . . 20
6866, 67sseldd 3351 . . . . . . . . . . . . . . . . . . 19
69 ssun2 3513 . . . . . . . . . . . . . . . . . . . . . 22
7069a1i 11 . . . . . . . . . . . . . . . . . . . . 21
7110, 12pclssN 30764 . . . . . . . . . . . . . . . . . . . . 21
7255, 70, 59, 71syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20
73 simp13 990 . . . . . . . . . . . . . . . . . . . 20
7472, 73sseldd 3351 . . . . . . . . . . . . . . . . . . 19
75 simp3r 987 . . . . . . . . . . . . . . . . . . 19
76 eqid 2438 . . . . . . . . . . . . . . . . . . . 20
77 eqid 2438 . . . . . . . . . . . . . . . . . . . 20
7876, 77, 10, 11psubspi2N 30618 . . . . . . . . . . . . . . . . . . 19
7955, 61, 62, 68, 74, 75, 78syl33anc 1200 . . . . . . . . . . . . . . . . . 18
80 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20
8180eleq2d 2505 . . . . . . . . . . . . . . . . . . 19
8281rspcev 3054 . . . . . . . . . . . . . . . . . 18
8354, 79, 82syl2anc 644 . . . . . . . . . . . . . . . . 17
84 eliun 4099 . . . . . . . . . . . . . . . . 17
8583, 84sylibr 205 . . . . . . . . . . . . . . . 16
86853exp 1153 . . . . . . . . . . . . . . 15
8786exp5c 601 . . . . . . . . . . . . . 14
88873exp 1153 . . . . . . . . . . . . 13
8940, 88syl5 31 . . . . . . . . . . . 12
9089rexlimdv 2831 . . . . . . . . . . 11
9190com24 84 . . . . . . . . . 10
9236, 91syl5 31 . . . . . . . . 9
9392rexlimdv 2831 . . . . . . . 8
9493imp3a 422 . . . . . . 7
9532, 94syl5bi 210 . . . . . 6
9695ralrimdv 2797 . . . . 5
9796ralrimivv 2799 . . . 4
9876, 77, 10, 11ispsubsp 30615 . . . . 5
9998adantr 453 . . . 4
10021, 97, 99mpbir2and 890 . . 3
101 snfi 7190 . . . . . . . . 9
102101a1i 11 . . . . . . . 8
103 snelpwi 4412 . . . . . . . . 9
104103adantl 454 . . . . . . . 8
105 elin 3532 . . . . . . . 8
106102, 104, 105sylanbrc 647 . . . . . . 7
10748snid 3843 . . . . . . . 8
108 simpll 732 . . . . . . . . 9
109 ssel2 3345 . . . . . . . . . . 11
110109adantll 696 . . . . . . . . . 10
11110, 11snatpsubN 30620 . . . . . . . . . 10
112108, 110, 111syl2anc 644 . . . . . . . . 9
11311, 12pclidN 30766 . . . . . . . . 9
114108, 112, 113syl2anc 644 . . . . . . . 8
115107, 114syl5eleqr 2525 . . . . . . 7
116 fveq2 5731 . . . . . . . . 9
117116eleq2d 2505 . . . . . . . 8
118117rspcev 3054 . . . . . . 7
119106, 115, 118syl2anc 644 . . . . . 6
120119ex 425 . . . . 5
121 eliun 4099 . . . . 5
122120, 121syl6ibr 220 . . . 4
123122ssrdv 3356 . . 3
124 simpr 449 . . . . . . . . . 10
125 simplr 733 . . . . . . . . . 10
12610, 12pclssN 30764 . . . . . . . . . 10
1276, 124, 125, 126syl3anc 1185 . . . . . . . . 9
128127sseld 3349 . . . . . . . 8
129128ex 425 . . . . . . 7
1305, 129syl5 31 . . . . . 6
131130rexlimdv 2831 . . . . 5
132121, 131syl5bi 210 . . . 4
133132ssrdv 3356 . . 3
13411, 12pclbtwnN 30767 . . 3
1351, 100, 123, 133, 134syl22anc 1186 . 2
136135eqcomd 2443 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  wral 2707  wrex 2708   cun 3320   cin 3321   wss 3322  cpw 3801  csn 3816  ciun 4095   class class class wbr 4215  cfv 5457  (class class class)co 6084  cfn 7112  cple 13541  cjn 14406  catm 30134  cal 30135  cpsubsp 30366  cpclN 30757 This theorem is referenced by:  pclcmpatN  30771 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-undef 6546  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-oadd 6731  df-er 6908  df-en 7113  df-fin 7116  df-poset 14408  df-plt 14420  df-lub 14436  df-join 14438  df-lat 14480  df-covers 30137  df-ats 30138  df-atl 30169  df-psubsp 30373  df-pclN 30758
 Copyright terms: Public domain W3C validator