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

Theorem fmfnfm 17992
 Description: A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypotheses
Ref Expression
fmfnfm.b
fmfnfm.l
fmfnfm.f
fmfnfm.fm
Assertion
Ref Expression
fmfnfm
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fmfnfm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmfnfm.b . . . . . 6
2 fbsspw 17866 . . . . . 6
31, 2syl 16 . . . . 5
4 elfvdm 5759 . . . . . . . 8
51, 4syl 16 . . . . . . 7
6 fmfnfm.l . . . . . . 7
7 fmfnfm.f . . . . . . 7
8 fmfnfm.fm . . . . . . . 8
9 ffn 5593 . . . . . . . . . . 11
10 dffn4 5661 . . . . . . . . . . 11
119, 10sylib 190 . . . . . . . . . 10
12 foima 5660 . . . . . . . . . 10
137, 11, 123syl 19 . . . . . . . . 9
14 filtop 17889 . . . . . . . . . . 11
156, 14syl 16 . . . . . . . . . 10
16 fgcl 17912 . . . . . . . . . . 11
17 filtop 17889 . . . . . . . . . . 11
181, 16, 173syl 19 . . . . . . . . . 10
19 eqid 2438 . . . . . . . . . . 11
2019imaelfm 17985 . . . . . . . . . 10
2115, 1, 7, 18, 20syl31anc 1188 . . . . . . . . 9
2213, 21eqeltrrd 2513 . . . . . . . 8
238, 22sseldd 3351 . . . . . . 7
24 rnelfmlem 17986 . . . . . . 7
255, 6, 7, 23, 24syl31anc 1188 . . . . . 6
26 fbsspw 17866 . . . . . 6
2725, 26syl 16 . . . . 5
283, 27unssd 3525 . . . 4
29 ssun1 3512 . . . . 5
30 fbasne0 17864 . . . . . 6
311, 30syl 16 . . . . 5
32 ssn0 3662 . . . . 5
3329, 31, 32sylancr 646 . . . 4
34 vex 2961 . . . . . . . . 9
35 eqid 2438 . . . . . . . . . 10
3635elrnmpt 5119 . . . . . . . . 9
3734, 36ax-mp 8 . . . . . . . 8
38 0nelfil 17883 . . . . . . . . . . . . . 14
396, 38syl 16 . . . . . . . . . . . . 13
4039ad2antrr 708 . . . . . . . . . . . 12
416adantr 453 . . . . . . . . . . . . . . 15
428adantr 453 . . . . . . . . . . . . . . . 16
4315, 1, 73jca 1135 . . . . . . . . . . . . . . . . . 18
4443adantr 453 . . . . . . . . . . . . . . . . 17
45 ssfg 17906 . . . . . . . . . . . . . . . . . . 19
461, 45syl 16 . . . . . . . . . . . . . . . . . 18
4746sselda 3350 . . . . . . . . . . . . . . . . 17
4819imaelfm 17985 . . . . . . . . . . . . . . . . 17
4944, 47, 48syl2anc 644 . . . . . . . . . . . . . . . 16
5042, 49sseldd 3351 . . . . . . . . . . . . . . 15
5141, 50jca 520 . . . . . . . . . . . . . 14
52 filin 17888 . . . . . . . . . . . . . . 15
53523expa 1154 . . . . . . . . . . . . . 14
5451, 53sylan 459 . . . . . . . . . . . . 13
55 eleq1 2498 . . . . . . . . . . . . 13
5654, 55syl5ibcom 213 . . . . . . . . . . . 12
5740, 56mtod 171 . . . . . . . . . . 11
58 neq0 3640 . . . . . . . . . . . 12
59 elin 3532 . . . . . . . . . . . . . 14
60 ffun 5595 . . . . . . . . . . . . . . . . . 18
61 fvelima 5780 . . . . . . . . . . . . . . . . . . 19
6261ex 425 . . . . . . . . . . . . . . . . . 18
637, 60, 623syl 19 . . . . . . . . . . . . . . . . 17
6463ad2antrr 708 . . . . . . . . . . . . . . . 16
657, 60syl 16 . . . . . . . . . . . . . . . . . . . . 21
6665ad3antrrr 712 . . . . . . . . . . . . . . . . . . . 20
67 fbelss 17867 . . . . . . . . . . . . . . . . . . . . . . . 24
681, 67sylan 459 . . . . . . . . . . . . . . . . . . . . . . 23
69 fdm 5597 . . . . . . . . . . . . . . . . . . . . . . . . 25
707, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
7170adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
7268, 71sseqtr4d 3387 . . . . . . . . . . . . . . . . . . . . . 22
7372adantr 453 . . . . . . . . . . . . . . . . . . . . 21
7473sselda 3350 . . . . . . . . . . . . . . . . . . . 20
75 fvimacnv 5847 . . . . . . . . . . . . . . . . . . . 20
7666, 74, 75syl2anc 644 . . . . . . . . . . . . . . . . . . 19
77 inelcm 3684 . . . . . . . . . . . . . . . . . . . . 21
7877ex 425 . . . . . . . . . . . . . . . . . . . 20
7978adantl 454 . . . . . . . . . . . . . . . . . . 19
8076, 79sylbid 208 . . . . . . . . . . . . . . . . . 18
81 eleq1 2498 . . . . . . . . . . . . . . . . . . 19
8281imbi1d 310 . . . . . . . . . . . . . . . . . 18
8380, 82syl5ibcom 213 . . . . . . . . . . . . . . . . 17
8483rexlimdva 2832 . . . . . . . . . . . . . . . 16
8564, 84syld 43 . . . . . . . . . . . . . . 15
8685imp3a 422 . . . . . . . . . . . . . 14
8759, 86syl5bi 210 . . . . . . . . . . . . 13
8887exlimdv 1647 . . . . . . . . . . . 12
8958, 88syl5bi 210 . . . . . . . . . . 11
9057, 89mpd 15 . . . . . . . . . 10
91 ineq2 3538 . . . . . . . . . . 11
9291neeq1d 2616 . . . . . . . . . 10
9390, 92syl5ibrcom 215 . . . . . . . . 9
9493rexlimdva 2832 . . . . . . . 8
9537, 94syl5bi 210 . . . . . . 7
9695expimpd 588 . . . . . 6
9796ralrimivv 2799 . . . . 5
98 fbunfip 17903 . . . . . 6
991, 25, 98syl2anc 644 . . . . 5
10097, 99mpbird 225 . . . 4
101 fsubbas 17901 . . . . 5
1021, 4, 1013syl 19 . . . 4
10328, 33, 100, 102mpbir3and 1138 . . 3
104 fgcl 17912 . . 3
105103, 104syl 16 . 2
106 unexg 4712 . . . . . 6
1071, 25, 106syl2anc 644 . . . . 5
108 ssfii 7426 . . . . 5
109107, 108syl 16 . . . 4
111 ssfg 17906 . . . 4
112103, 111syl 16 . . 3
113110, 112sstrd 3360 . 2
1141, 6, 7, 8fmfnfmlem4 17991 . . . . 5
115 elfm 17981 . . . . . 6
11615, 103, 7, 115syl3anc 1185 . . . . 5
117114, 116bitr4d 249 . . . 4
118117eqrdv 2436 . . 3
119 eqid 2438 . . . . 5
120119fmfg 17983 . . . 4
12115, 103, 7, 120syl3anc 1185 . . 3
122118, 121eqtrd 2470 . 2
123 sseq2 3372 . . . 4
124 fveq2 5730 . . . . 5
125124eqeq2d 2449 . . . 4
126123, 125anbi12d 693 . . 3
127126rspcev 3054 . 2
128105, 113, 122, 127syl12anc 1183 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726   wne 2601  wral 2707  wrex 2708  cvv 2958   cun 3320   cin 3321   wss 3322  c0 3630  cpw 3801   cmpt 4268  ccnv 4879   cdm 4880   crn 4881  cima 4883   wfun 5450   wfn 5451  wf 5452  wfo 5454  cfv 5456  (class class class)co 6083  cfi 7417  cfbas 16691  cfg 16692  cfil 17879   cfm 17967 This theorem is referenced by:  fmufil  17993  cnpfcf  18075 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703 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 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-recs 6635  df-rdg 6670  df-1o 6726  df-oadd 6730  df-er 6907  df-en 7112  df-fin 7115  df-fi 7418  df-fbas 16701  df-fg 16702  df-fil 17880  df-fm 17972
 Copyright terms: Public domain W3C validator