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

Theorem i1faddlem 20871
Description: Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
i1fadd.1
i1fadd.2
Assertion
Ref Expression
i1faddlem
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem i1faddlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 i1fadd.1 . . . . . . . . 9
2 i1ff 20854 . . . . . . . . 9
31, 2syl 16 . . . . . . . 8
4 ffn 5529 . . . . . . . 8
53, 4syl 16 . . . . . . 7
6 i1fadd.2 . . . . . . . . 9
7 i1ff 20854 . . . . . . . . 9
86, 7syl 16 . . . . . . . 8
9 ffn 5529 . . . . . . . 8
108, 9syl 16 . . . . . . 7
11 reex 9319 . . . . . . . 8
1211a1i 11 . . . . . . 7
13 inidm 3536 . . . . . . 7
145, 10, 12, 12, 13offn 6301 . . . . . 6
1514adantr 455 . . . . 5
16 fniniseg 5794 . . . . 5
1715, 16syl 16 . . . 4
1810ad2antrr 710 . . . . . . . 8
19 simprl 740 . . . . . . . 8
20 fnfvelrn 5810 . . . . . . . 8
2118, 19, 20syl2anc 646 . . . . . . 7
22 simprr 741 . . . . . . . . . . . 12
23 eqidd 2423 . . . . . . . . . . . . . 14
24 eqidd 2423 . . . . . . . . . . . . . 14
255, 10, 12, 12, 13, 23, 24ofval 6299 . . . . . . . . . . . . 13
2625ad2ant2r 731 . . . . . . . . . . . 12
2722, 26eqtr3d 2456 . . . . . . . . . . 11
2827oveq1d 6076 . . . . . . . . . 10
29 ax-resscn 9285 . . . . . . . . . . . . . 14
30 fss 5537 . . . . . . . . . . . . . 14
313, 29, 30sylancl 647 . . . . . . . . . . . . 13
3231ad2antrr 710 . . . . . . . . . . . 12
3332, 19ffvelrnd 5814 . . . . . . . . . . 11
34 fss 5537 . . . . . . . . . . . . . 14
358, 29, 34sylancl 647 . . . . . . . . . . . . 13
3635ad2antrr 710 . . . . . . . . . . . 12
3736, 19ffvelrnd 5814 . . . . . . . . . . 11
3833, 37pncand 9666 . . . . . . . . . 10
3928, 38eqtr2d 2455 . . . . . . . . 9
405ad2antrr 710 . . . . . . . . . 10
41 fniniseg 5794 . . . . . . . . . 10
4240, 41syl 16 . . . . . . . . 9
4319, 39, 42mpbir2and 898 . . . . . . . 8
44 eqidd 2423 . . . . . . . . 9
45 fniniseg 5794 . . . . . . . . . 10
4618, 45syl 16 . . . . . . . . 9
4719, 44, 46mpbir2and 898 . . . . . . . 8
4843, 47elind 3517 . . . . . . 7
49 oveq2 6069 . . . . . . . . . . . 12
5049sneqd 3866 . . . . . . . . . . 11
5150imaeq2d 5141 . . . . . . . . . 10
52 sneq 3864 . . . . . . . . . . 11
5352imaeq2d 5141 . . . . . . . . . 10
5451, 53ineq12d 3530 . . . . . . . . 9
5554eleq2d 2489 . . . . . . . 8
5655rspcev 3051 . . . . . . 7
5721, 48, 56syl2anc 646 . . . . . 6
5857ex 427 . . . . 5
59 elin 3516 . . . . . . 7
605adantr 455 . . . . . . . . . 10
61 fniniseg 5794 . . . . . . . . . 10
6260, 61syl 16 . . . . . . . . 9
6310adantr 455 . . . . . . . . . 10
64 fniniseg 5794 . . . . . . . . . 10
6563, 64syl 16 . . . . . . . . 9
6662, 65anbi12d 695 . . . . . . . 8
67 anandi 809 . . . . . . . . 9
68 simprl 740 . . . . . . . . . . 11
6925ad2ant2r 731 . . . . . . . . . . . 12
70 simprrl 748 . . . . . . . . . . . . 13
71 simprrr 749 . . . . . . . . . . . . 13
7270, 71oveq12d 6079 . . . . . . . . . . . 12
73 simplr 739 . . . . . . . . . . . . 13
7435ad2antrr 710 . . . . . . . . . . . . . . 15
7574, 68ffvelrnd 5814 . . . . . . . . . . . . . 14
7671, 75eqeltrrd 2497 . . . . . . . . . . . . 13
7773, 76npcand 9669 . . . . . . . . . . . 12
7869, 72, 773eqtrd 2458 . . . . . . . . . . 11
7968, 78jca 522 . . . . . . . . . 10
8079ex 427 . . . . . . . . 9
8167, 80syl5bir 212 . . . . . . . 8
8266, 81sylbid 209 . . . . . . 7
8359, 82syl5bi 211 . . . . . 6
8483rexlimdvw 2823 . . . . 5
8558, 84impbid 185 . . . 4
8617, 85bitrd 247 . . 3
87 eliun 4150 . . 3
8886, 87syl6bbr 257 . 2
8988eqrdv 2420 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362  =wceq 1687  e.wcel 1749  E.wrex 2695   cvv 2951  i^icin 3304  C_wss 3305  {csn 3853  U_ciun 4146  `'ccnv 4810  domcdm 4811  rancrn 4812  "cima 4814  Fnwfn 5385  -->wf 5386  `cfv 5390  (class class class)co 6061  oFcof 6288   cc 9226   cr 9227   caddc 9231   cmin 9541   citg1 20795
This theorem is referenced by:  i1fadd  20873  itg1addlem4  20877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-po 4612  df-so 4613  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-of 6290  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-ltxr 9369  df-sub 9543  df-sum 13105  df-itg1 20800
  Copyright terms: Public domain W3C validator