Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1280 Structured version   Unicode version

Theorem bnj1280 29781
 Description: Technical lemma for bnj60 29823. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1280.1
bnj1280.2
bnj1280.3
bnj1280.4
bnj1280.5
bnj1280.6
bnj1280.7
bnj1280.17
Assertion
Ref Expression
bnj1280
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,   ,,   ,   ,   ,   ,,   ,,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,)   (,,)   (,,,,,)   (,,,)   (,,,)   (,,,,,)   (,,)   (,,,)

Proof of Theorem bnj1280
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1280.1 . . . . . . . 8
2 bnj1280.2 . . . . . . . 8
3 bnj1280.3 . . . . . . . 8
4 bnj1280.4 . . . . . . . 8
5 bnj1280.5 . . . . . . . 8
6 bnj1280.6 . . . . . . . 8
7 bnj1280.7 . . . . . . . 8
81, 2, 3, 4, 5, 6, 7bnj1286 29780 . . . . . . 7
98sseld 3406 . . . . . 6
10 bnj1280.17 . . . . . . . . 9
11 disj1 3780 . . . . . . . . 9
1210, 11sylib 199 . . . . . . . 8
131219.21bi 1924 . . . . . . 7
14 fveq2 5825 . . . . . . . . . . 11
15 fveq2 5825 . . . . . . . . . . 11
1614, 15neeq12d 2662 . . . . . . . . . 10
1716, 5elrab2 3173 . . . . . . . . 9
1817notbii 297 . . . . . . . 8
19 imnan 423 . . . . . . . 8
20 nne 2605 . . . . . . . . 9
2120imbi2i 313 . . . . . . . 8
2218, 19, 213bitr2i 276 . . . . . . 7
2313, 22syl6ib 229 . . . . . 6
249, 23mpdd 41 . . . . 5
2524imp 430 . . . 4
26 fvres 5839 . . . . . 6
279, 26syl6 34 . . . . 5
2827imp 430 . . . 4
29 fvres 5839 . . . . . 6
309, 29syl6 34 . . . . 5
3130imp 430 . . . 4
3225, 28, 313eqtr4d 2472 . . 3
3332ralrimiva 2779 . 2
348resabs1d 5096 . . . 4
358resabs1d 5096 . . . 4
3634, 35eqeq12d 2443 . . 3
371, 2, 3, 4, 5, 6, 7bnj1256 29776 . . . . . . 7
384bnj1292 29579 . . . . . . . . 9
39 fndm 5636 . . . . . . . . 9
4038, 39syl5sseq 3455 . . . . . . . 8
41 fnssres 5650 . . . . . . . 8
4240, 41mpdan 672 . . . . . . 7
4337, 42bnj31 29477 . . . . . 6
4443bnj1265 29576 . . . . 5
457, 44bnj835 29522 . . . 4
461, 2, 3, 4, 5, 6, 7bnj1259 29777 . . . . . . 7
474bnj1293 29580 . . . . . . . . 9
48 fndm 5636 . . . . . . . . 9
4947, 48syl5sseq 3455 . . . . . . . 8
50 fnssres 5650 . . . . . . . 8
5149, 50mpdan 672 . . . . . . 7
5246, 51bnj31 29477 . . . . . 6
5352bnj1265 29576 . . . . 5
547, 53bnj835 29522 . . . 4
55 fvreseq 5943 . . . 4
5645, 54, 8, 55syl21anc 1263 . . 3
5736, 56bitr3d 258 . 2
5833, 57mpbird 235 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982  wal 1435   wceq 1437   wcel 1872  cab 2414   wne 2599  wral 2714  wrex 2715  crab 2718   cin 3378   wss 3379  c0 3704  cop 3947   class class class wbr 4366   cdm 4796   cres 4798   wfn 5539  cfv 5544   w-bnj17 29443   c-bnj14 29445   w-bnj15 29449 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-fv 5552  df-bnj17 29444 This theorem is referenced by:  bnj1311  29785
 Copyright terms: Public domain W3C validator