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

Theorem f1lindf 19373
 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 2450 . . . . . . 7
21lindff 19366 . . . . . 6 LIndF
32ancoms 455 . . . . 5 LIndF
433adant3 1027 . . . 4 LIndF
5 f1f 5777 . . . . 5
653ad2ant3 1030 . . . 4 LIndF
7 fco 5737 . . . 4
84, 6, 7syl2anc 666 . . 3 LIndF
9 ffdm 5741 . . . 4
109simpld 461 . . 3
118, 10syl 17 . 2 LIndF
12 simpl2 1011 . . . . 5 LIndF Scalar Scalar LIndF
136adantr 467 . . . . . . 7 LIndF
14 fdm 5731 . . . . . . . . . 10
158, 14syl 17 . . . . . . . . 9 LIndF
1615eleq2d 2513 . . . . . . . 8 LIndF
1716biimpa 487 . . . . . . 7 LIndF
1813, 17ffvelrnd 6021 . . . . . 6 LIndF
1918adantrr 722 . . . . 5 LIndF Scalar Scalar
20 eldifi 3554 . . . . . 6 Scalar Scalar Scalar
2120ad2antll 734 . . . . 5 LIndF Scalar Scalar Scalar
22 eldifsni 4097 . . . . . 6 Scalar Scalar Scalar
2322ad2antll 734 . . . . 5 LIndF Scalar Scalar Scalar
24 eqid 2450 . . . . . 6
25 eqid 2450 . . . . . 6
26 eqid 2450 . . . . . 6 Scalar Scalar
27 eqid 2450 . . . . . 6 Scalar Scalar
28 eqid 2450 . . . . . 6 Scalar Scalar
2924, 25, 26, 27, 28lindfind 19367 . . . . 5 LIndF Scalar Scalar
3012, 19, 21, 23, 29syl22anc 1268 . . . 4 LIndF Scalar Scalar
31 f1fn 5778 . . . . . . . . . . 11
32313ad2ant3 1030 . . . . . . . . . 10 LIndF
3332adantr 467 . . . . . . . . 9 LIndF
34 fvco2 5938 . . . . . . . . 9
3533, 17, 34syl2anc 666 . . . . . . . 8 LIndF
3635oveq2d 6304 . . . . . . 7 LIndF
3736eleq1d 2512 . . . . . 6 LIndF
38 simpl1 1010 . . . . . . . . 9 LIndF
39 imassrn 5178 . . . . . . . . . . 11
40 frn 5733 . . . . . . . . . . . 12
414, 40syl 17 . . . . . . . . . . 11 LIndF
4239, 41syl5ss 3442 . . . . . . . . . 10 LIndF
4342adantr 467 . . . . . . . . 9 LIndF
44 imaco 5339 . . . . . . . . . 10
4515difeq1d 3549 . . . . . . . . . . . . . . 15 LIndF
4645imaeq2d 5167 . . . . . . . . . . . . . 14 LIndF
47 df-f1 5586 . . . . . . . . . . . . . . . . 17
4847simprbi 466 . . . . . . . . . . . . . . . 16
49483ad2ant3 1030 . . . . . . . . . . . . . . 15 LIndF
50 imadif 5656 . . . . . . . . . . . . . . 15
5149, 50syl 17 . . . . . . . . . . . . . 14 LIndF
5246, 51eqtrd 2484 . . . . . . . . . . . . 13 LIndF
5352adantr 467 . . . . . . . . . . . 12 LIndF
54 fnsnfv 5923 . . . . . . . . . . . . . . 15
5532, 54sylan 474 . . . . . . . . . . . . . 14 LIndF
5655difeq2d 3550 . . . . . . . . . . . . 13 LIndF
57 imassrn 5178 . . . . . . . . . . . . . . 15
586adantr 467 . . . . . . . . . . . . . . . 16 LIndF
59 frn 5733 . . . . . . . . . . . . . . . 16
6058, 59syl 17 . . . . . . . . . . . . . . 15 LIndF
6157, 60syl5ss 3442 . . . . . . . . . . . . . 14 LIndF
6261ssdifd 3568 . . . . . . . . . . . . 13 LIndF
6356, 62eqsstr3d 3466 . . . . . . . . . . . 12 LIndF
6453, 63eqsstrd 3465 . . . . . . . . . . 11 LIndF
65 imass2 5203 . . . . . . . . . . 11
6664, 65syl 17 . . . . . . . . . 10 LIndF
6744, 66syl5eqss 3475 . . . . . . . . 9 LIndF
681, 25lspss 18200 . . . . . . . . 9
6938, 43, 67, 68syl3anc 1267 . . . . . . . 8 LIndF
7017, 69syldan 473 . . . . . . 7 LIndF
7170sseld 3430 . . . . . 6 LIndF
7237, 71sylbid 219 . . . . 5 LIndF
7372adantrr 722 . . . 4 LIndF Scalar Scalar
7430, 73mtod 181 . . 3 LIndF Scalar Scalar
7574ralrimivva 2808 . 2 LIndF Scalar Scalar
76 simp1 1007 . . 3 LIndF
77 rellindf 19359 . . . . . 6 LIndF
7877brrelexi 4874 . . . . 5 LIndF
79783ad2ant2 1029 . . . 4 LIndF
80 simp3 1009 . . . . . 6 LIndF
81 dmexg 6721 . . . . . . 7
8279, 81syl 17 . . . . . 6 LIndF
83 f1dmex 6760 . . . . . 6
8480, 82, 83syl2anc 666 . . . . 5 LIndF
85 fex 6136 . . . . 5
866, 84, 85syl2anc 666 . . . 4 LIndF
87 coexg 6741 . . . 4
8879, 86, 87syl2anc 666 . . 3 LIndF
891, 24, 25, 26, 28, 27islindf 19363 . . 3 LIndF Scalar Scalar
9076, 88, 89syl2anc 666 . 2 LIndF LIndF Scalar Scalar
9111, 75, 90mpbir2and 932 1 LIndF LIndF
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   w3a 984   wceq 1443   wcel 1886   wne 2621  wral 2736  cvv 3044   cdif 3400   wss 3403  csn 3967   class class class wbr 4401  ccnv 4832   cdm 4833   crn 4834  cima 4836   ccom 4837   wfun 5575   wfn 5576  wf 5577  wf1 5578  cfv 5581  (class class class)co 6288  cbs 15114  Scalarcsca 15186  cvsca 15187  c0g 15331  clmod 18084  clspn 18187   LIndF clindf 19355 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-slot 15118  df-base 15119  df-0g 15333  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-grp 16666  df-lmod 18086  df-lss 18149  df-lsp 18188  df-lindf 19357 This theorem is referenced by:  lindfres  19374  f1linds  19376
 Copyright terms: Public domain W3C validator