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

Theorem islinds 18347
 Description: Property of an independent set of vectors in terms of an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Hypothesis
Ref Expression
islinds.b
Assertion
Ref Expression
islinds LIndS LIndF

Proof of Theorem islinds
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3077 . . . . 5
2 fveq2 5789 . . . . . . . 8
32pweqd 3963 . . . . . . 7
4 breq2 4394 . . . . . . 7 LIndF LIndF
53, 4rabeqbidv 3063 . . . . . 6 LIndF LIndF
6 df-linds 18345 . . . . . 6 LIndS LIndF
7 fvex 5799 . . . . . . . 8
87pwex 4573 . . . . . . 7
98rabex 4541 . . . . . 6 LIndF
105, 6, 9fvmpt 5873 . . . . 5 LIndS LIndF
111, 10syl 16 . . . 4 LIndS LIndF
1211eleq2d 2521 . . 3 LIndS LIndF
13 reseq2 5203 . . . . 5
1413breq1d 4400 . . . 4 LIndF LIndF
1514elrab 3214 . . 3 LIndF LIndF
1612, 15syl6bb 261 . 2 LIndS LIndF
177elpw2 4554 . . . 4
18 islinds.b . . . . 5
1918sseq2i 3479 . . . 4
2017, 19bitr4i 252 . . 3
2120anbi1i 695 . 2 LIndF LIndF
2216, 21syl6bb 261 1 LIndS LIndF
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758  crab 2799  cvv 3068   wss 3426  cpw 3958   class class class wbr 4390   cid 4729   cres 4940  cfv 5516  cbs 14276   LIndF clindf 18342  LIndSclinds 18343 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-res 4950  df-iota 5479  df-fun 5518  df-fv 5524  df-linds 18345 This theorem is referenced by:  linds1  18348  linds2  18349  islinds2  18351  lindsss  18362  lindsmm  18366  lsslinds  18369
 Copyright terms: Public domain W3C validator