Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspval Structured version   Unicode version

Theorem sspval 26345
 Description: The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
sspval.g
sspval.s
sspval.n CV
sspval.h
Assertion
Ref Expression
sspval CV
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem sspval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sspval.h . 2
2 fveq2 5877 . . . . . . 7
3 sspval.g . . . . . . 7
42, 3syl6eqr 2481 . . . . . 6
54sseq2d 3492 . . . . 5
6 fveq2 5877 . . . . . . 7
7 sspval.s . . . . . . 7
86, 7syl6eqr 2481 . . . . . 6
98sseq2d 3492 . . . . 5
10 fveq2 5877 . . . . . . 7 CV CV
11 sspval.n . . . . . . 7 CV
1210, 11syl6eqr 2481 . . . . . 6 CV
1312sseq2d 3492 . . . . 5 CV CV CV
145, 9, 133anbi123d 1335 . . . 4 CV CV CV
1514rabbidv 3072 . . 3 CV CV CV
16 df-ssp 26344 . . 3 CV CV
17 fvex 5887 . . . . . . . 8
183, 17eqeltri 2506 . . . . . . 7
1918pwex 4603 . . . . . 6
20 fvex 5887 . . . . . . . 8
217, 20eqeltri 2506 . . . . . . 7
2221pwex 4603 . . . . . 6
2319, 22xpex 6605 . . . . 5
24 fvex 5887 . . . . . . 7 CV
2511, 24eqeltri 2506 . . . . . 6
2625pwex 4603 . . . . 5
2723, 26xpex 6605 . . . 4
28 rabss 3538 . . . . 5 CV CV
29 fvex 5887 . . . . . . . . . 10
3029elpw 3985 . . . . . . . . 9
31 fvex 5887 . . . . . . . . . 10
3231elpw 3985 . . . . . . . . 9
33 opelxpi 4881 . . . . . . . . 9
3430, 32, 33syl2anbr 482 . . . . . . . 8
35 fvex 5887 . . . . . . . . . 10 CV
3635elpw 3985 . . . . . . . . 9 CV CV
3736biimpri 209 . . . . . . . 8 CV CV
38 opelxpi 4881 . . . . . . . 8 CV CV
3934, 37, 38syl2an 479 . . . . . . 7 CV CV
40393impa 1200 . . . . . 6 CV CV
41 eqid 2422 . . . . . . . 8
42 eqid 2422 . . . . . . . 8
43 eqid 2422 . . . . . . . 8 CV CV
4441, 42, 43nvop 26289 . . . . . . 7 CV
4544eleq1d 2491 . . . . . 6 CV
4640, 45syl5ibr 224 . . . . 5 CV
4728, 46mprgbir 2789 . . . 4 CV
4827, 47ssexi 4565 . . 3 CV
4915, 16, 48fvmpt 5960 . 2 CV
501, 49syl5eq 2475 1 CV
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868  crab 2779  cvv 3081   wss 3436  cpw 3979  cop 4002   cxp 4847  cfv 5597  cnv 26186  cpv 26187  cns 26189  CVcnmcv 26192  css 26343 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-fo 5603  df-fv 5605  df-oprab 6305  df-1st 6803  df-2nd 6804  df-vc 26148  df-nv 26194  df-va 26197  df-sm 26199  df-nmcv 26202  df-ssp 26344 This theorem is referenced by:  isssp  26346
 Copyright terms: Public domain W3C validator