Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  f1lindf Unicode version

Theorem f1lindf 27292
 Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Assertion
Ref Expression
f1lindf LIndF LIndF

Proof of Theorem f1lindf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2283 . . . . . . 7
21lindff 27285 . . . . . 6 LIndF
32ancoms 439 . . . . 5 LIndF
433adant3 975 . . . 4 LIndF
5 f1f 5437 . . . . 5
653ad2ant3 978 . . . 4 LIndF
7 fco 5398 . . . 4
84, 6, 7syl2anc 642 . . 3 LIndF
9 ffdm 5403 . . . 4
109simpld 445 . . 3
118, 10syl 15 . 2 LIndF
12 simpl2 959 . . . . 5 LIndF Scalar Scalar LIndF
136adantr 451 . . . . . . 7 LIndF
14 fdm 5393 . . . . . . . . . 10
158, 14syl 15 . . . . . . . . 9 LIndF
1615eleq2d 2350 . . . . . . . 8 LIndF
1716biimpa 470 . . . . . . 7 LIndF
18 ffvelrn 5663 . . . . . . 7
1913, 17, 18syl2anc 642 . . . . . 6 LIndF
2019adantrr 697 . . . . 5 LIndF Scalar Scalar
21 eldifi 3298 . . . . . 6 Scalar Scalar Scalar
2221ad2antll 709 . . . . 5 LIndF Scalar Scalar Scalar
23 eldifsni 3750 . . . . . 6 Scalar Scalar Scalar
2423ad2antll 709 . . . . 5 LIndF Scalar Scalar Scalar
25 eqid 2283 . . . . . 6
26 eqid 2283 . . . . . 6
27 eqid 2283 . . . . . 6 Scalar Scalar
28 eqid 2283 . . . . . 6 Scalar Scalar
29 eqid 2283 . . . . . 6 Scalar Scalar
3025, 26, 27, 28, 29lindfind 27286 . . . . 5 LIndF Scalar Scalar
3112, 20, 22, 24, 30syl22anc 1183 . . . 4 LIndF Scalar Scalar
32 f1fn 5438 . . . . . . . . . . 11
33323ad2ant3 978 . . . . . . . . . 10 LIndF
3433adantr 451 . . . . . . . . 9 LIndF
35 fvco2 5594 . . . . . . . . 9
3634, 17, 35syl2anc 642 . . . . . . . 8 LIndF
3736oveq2d 5874 . . . . . . 7 LIndF
3837eleq1d 2349 . . . . . 6 LIndF
39 simpl1 958 . . . . . . . . 9 LIndF
40 imassrn 5025 . . . . . . . . . . 11
41 frn 5395 . . . . . . . . . . . 12
424, 41syl 15 . . . . . . . . . . 11 LIndF
4340, 42syl5ss 3190 . . . . . . . . . 10 LIndF
4443adantr 451 . . . . . . . . 9 LIndF
45 imaco 5178 . . . . . . . . . 10
4615difeq1d 3293 . . . . . . . . . . . . . . 15 LIndF
4746imaeq2d 5012 . . . . . . . . . . . . . 14 LIndF
48 df-f1 5260 . . . . . . . . . . . . . . . . 17
4948simprbi 450 . . . . . . . . . . . . . . . 16
50493ad2ant3 978 . . . . . . . . . . . . . . 15 LIndF
51 imadif 5327 . . . . . . . . . . . . . . 15
5250, 51syl 15 . . . . . . . . . . . . . 14 LIndF
5347, 52eqtrd 2315 . . . . . . . . . . . . 13 LIndF
5453adantr 451 . . . . . . . . . . . 12 LIndF
55 fnsnfv 5582 . . . . . . . . . . . . . . 15
5633, 55sylan 457 . . . . . . . . . . . . . 14 LIndF
5756difeq2d 3294 . . . . . . . . . . . . 13 LIndF
58 imassrn 5025 . . . . . . . . . . . . . . 15
596adantr 451 . . . . . . . . . . . . . . . 16 LIndF
60 frn 5395 . . . . . . . . . . . . . . . 16
6159, 60syl 15 . . . . . . . . . . . . . . 15 LIndF
6258, 61syl5ss 3190 . . . . . . . . . . . . . 14 LIndF
63 ssdif 3311 . . . . . . . . . . . . . 14
6462, 63syl 15 . . . . . . . . . . . . 13 LIndF
6557, 64eqsstr3d 3213 . . . . . . . . . . . 12 LIndF
6654, 65eqsstrd 3212 . . . . . . . . . . 11 LIndF
67 imass2 5049 . . . . . . . . . . 11
6866, 67syl 15 . . . . . . . . . 10 LIndF
6945, 68syl5eqss 3222 . . . . . . . . 9 LIndF
701, 26lspss 15741 . . . . . . . . 9
7139, 44, 69, 70syl3anc 1182 . . . . . . . 8 LIndF
7217, 71syldan 456 . . . . . . 7 LIndF
7372sseld 3179 . . . . . 6 LIndF
7438, 73sylbid 206 . . . . 5 LIndF
7574adantrr 697 . . . 4 LIndF Scalar Scalar
7631, 75mtod 168 . . 3 LIndF Scalar Scalar
7776ralrimivva 2635 . 2 LIndF Scalar Scalar
78 simp1 955 . . 3 LIndF
79 rellindf 27278 . . . . . 6 LIndF
8079brrelexi 4729 . . . . 5 LIndF
81803ad2ant2 977 . . . 4 LIndF
82 simp3 957 . . . . . 6 LIndF
83 dmexg 4939 . . . . . . 7
8481, 83syl 15 . . . . . 6 LIndF
85 f1dmex 5751 . . . . . 6
8682, 84, 85syl2anc 642 . . . . 5 LIndF
87 fex 5749 . . . . 5
886, 86, 87syl2anc 642 . . . 4 LIndF
89 coexg 5215 . . . 4
9081, 88, 89syl2anc 642 . . 3 LIndF
911, 25, 26, 27, 29, 28islindf 27282 . . 3 LIndF Scalar Scalar
9278, 90, 91syl2anc 642 . 2 LIndF LIndF Scalar Scalar
9311, 77, 92mpbir2and 888 1 LIndF LIndF
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684   wne 2446  wral 2543  cvv 2788   cdif 3149   wss 3152  csn 3640   class class class wbr 4023  ccnv 4688   cdm 4689   crn 4690  cima 4692   ccom 4693   wfun 5249   wfn 5250  wf 5251  wf1 5252  cfv 5255  (class class class)co 5858  cbs 13148  Scalarcsca 13211  cvsca 13212  c0g 13400  clmod 15627  clspn 15728   LIndF clindf 27274 This theorem is referenced by:  lindfres  27293  f1linds  27295 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-riota 6304  df-slot 13152  df-base 13153  df-0g 13404  df-mnd 14367  df-grp 14489  df-lmod 15629  df-lss 15690  df-lsp 15729  df-lindf 27276
 Copyright terms: Public domain W3C validator