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

Theorem bnj1145 28785
 Description: Technical lemma for bnj69 28802. 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
bnj1145.1
bnj1145.2
bnj1145.3
bnj1145.4
bnj1145.5
bnj1145.6
Assertion
Ref Expression
bnj1145
Distinct variable groups:   ,,,,,   ,,   ,,,,,   ,,,,   ,   ,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,)   ()

Proof of Theorem bnj1145
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1145.1 . . 3
2 bnj1145.2 . . 3
3 bnj1145.3 . . 3
4 bnj1145.4 . . 3
51, 2, 3, 4bnj882 28720 . 2
6 ss2iun 4001 . . . 4
7 bnj1145.5 . . . . . . 7
87, 4bnj1083 28770 . . . . . 6
92bnj1095 28575 . . . . . . . . . 10
109, 7bnj1096 28576 . . . . . . . . 9
1110nfi 1551 . . . . . . . 8
123bnj1098 28577 . . . . . . . . . . . . . . . . 17
137bnj1232 28598 . . . . . . . . . . . . . . . . . 18
14133anim3i 1139 . . . . . . . . . . . . . . . . 17
1512, 14bnj1101 28578 . . . . . . . . . . . . . . . 16
16 ancl 529 . . . . . . . . . . . . . . . 16
1715, 16bnj101 28511 . . . . . . . . . . . . . . 15
18 bnj1145.6 . . . . . . . . . . . . . . . . 17
1918imbi2i 303 . . . . . . . . . . . . . . . 16
2019exbii 1582 . . . . . . . . . . . . . . 15
2117, 20mpbir 200 . . . . . . . . . . . . . 14
22 bnj213 28676 . . . . . . . . . . . . . . . 16
2322bnj226 28524 . . . . . . . . . . . . . . 15
24 simpr 447 . . . . . . . . . . . . . . . . . . 19
2518, 24bnj833 28550 . . . . . . . . . . . . . . . . . 18
26 simp2 956 . . . . . . . . . . . . . . . . . . . 20
27133ad2ant3 978 . . . . . . . . . . . . . . . . . . . 20
283bnj923 28560 . . . . . . . . . . . . . . . . . . . . 21
29 elnn 4748 . . . . . . . . . . . . . . . . . . . . 21
3028, 29sylan2 460 . . . . . . . . . . . . . . . . . . . 20
3126, 27, 30syl2anc 642 . . . . . . . . . . . . . . . . . . 19
3218, 31bnj832 28549 . . . . . . . . . . . . . . . . . 18
33 vex 2867 . . . . . . . . . . . . . . . . . . . 20
3433bnj216 28522 . . . . . . . . . . . . . . . . . . 19
35 elnn 4748 . . . . . . . . . . . . . . . . . . 19
3634, 35sylan 457 . . . . . . . . . . . . . . . . . 18
3725, 32, 36syl2anc 642 . . . . . . . . . . . . . . . . 17
3818, 26bnj832 28549 . . . . . . . . . . . . . . . . . 18
3925, 38eqeltrrd 2433 . . . . . . . . . . . . . . . . 17
402bnj589 28703 . . . . . . . . . . . . . . . . . . . . . . 23
4140biimpi 186 . . . . . . . . . . . . . . . . . . . . . 22
4241bnj708 28547 . . . . . . . . . . . . . . . . . . . . 21
43 rsp 2679 . . . . . . . . . . . . . . . . . . . . 21
4442, 43syl 15 . . . . . . . . . . . . . . . . . . . 20
457, 44sylbi 187 . . . . . . . . . . . . . . . . . . 19
46453ad2ant3 978 . . . . . . . . . . . . . . . . . 18
4718, 46bnj832 28549 . . . . . . . . . . . . . . . . 17
4837, 39, 47mp2d 41 . . . . . . . . . . . . . . . 16
49 fveq2 5608 . . . . . . . . . . . . . . . . . 18
5049eqeq1d 2366 . . . . . . . . . . . . . . . . 17
5125, 50syl 15 . . . . . . . . . . . . . . . 16
5248, 51mpbird 223 . . . . . . . . . . . . . . 15
5323, 52bnj1262 28605 . . . . . . . . . . . . . 14
5421, 53bnj1023 28574 . . . . . . . . . . . . 13
55 3anass 938 . . . . . . . . . . . . . . 15
5655imbi1i 315 . . . . . . . . . . . . . 14
5756exbii 1582 . . . . . . . . . . . . 13
5854, 57mpbi 199 . . . . . . . . . . . 12
591biimpi 186 . . . . . . . . . . . . . . 15
607, 59bnj771 28556 . . . . . . . . . . . . . 14
61 fveq2 5608 . . . . . . . . . . . . . . 15
62 bnj213 28676 . . . . . . . . . . . . . . . 16
63 sseq1 3275 . . . . . . . . . . . . . . . 16
6462, 63mpbiri 224 . . . . . . . . . . . . . . 15
65 sseq1 3275 . . . . . . . . . . . . . . . 16
6665biimpar 471 . . . . . . . . . . . . . . 15
6761, 64, 66syl2an 463 . . . . . . . . . . . . . 14
6860, 67sylan2 460 . . . . . . . . . . . . 13
6968adantrl 696 . . . . . . . . . . . 12
7058, 69bnj1109 28580 . . . . . . . . . . 11
71 19.9v 1664 . . . . . . . . . . 11
7270, 71mpbi 199 . . . . . . . . . 10
7372expcom 424 . . . . . . . . 9
74 fndm 5425 . . . . . . . . . . 11
757, 74bnj770 28555 . . . . . . . . . 10
76 eleq2 2419 . . . . . . . . . . 11
7776imbi1d 308 . . . . . . . . . 10
7875, 77syl 15 . . . . . . . . 9
7973, 78mpbird 223 . . . . . . . 8
8011, 79ralrimi 2700 . . . . . . 7
8180exlimiv 1634 . . . . . 6
828, 81sylbi 187 . . . . 5
83 ss2iun 4001 . . . . . 6
84 bnj1143 28584 . . . . . 6
8583, 84syl6ss 3267 . . . . 5
8682, 85syl 15 . . . 4
876, 86mprg 2688 . . 3
884bnj1317 28616 . . . 4
8988bnj1146 28585 . . 3
9087, 89sstri 3264 . 2
915, 90eqsstri 3284 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wex 1541   wceq 1642   wcel 1710  cab 2344   wne 2521  wral 2619  wrex 2620   cdif 3225   wss 3228  c0 3531  csn 3716  ciun 3986   csuc 4476  com 4738   cdm 4771   wfn 5332  cfv 5337   w-bnj17 28473   c-bnj14 28475   c-bnj18 28481 This theorem is referenced by:  bnj1147  28786 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295  ax-un 4594 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-tr 4195  df-eprel 4387  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-iota 5301  df-fn 5340  df-fv 5345  df-bnj17 28474  df-bnj14 28476  df-bnj18 28482
 Copyright terms: Public domain W3C validator