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

Theorem bnj1018 29725
 Description: Technical lemma for bnj69 29771. 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
bnj1018.1
bnj1018.2
bnj1018.3
bnj1018.4
bnj1018.5
bnj1018.7
bnj1018.8
bnj1018.9
bnj1018.10
bnj1018.11
bnj1018.12
bnj1018.13
bnj1018.14
bnj1018.15
bnj1018.16
bnj1018.26
bnj1018.29
bnj1018.30
Assertion
Ref Expression
bnj1018
Distinct variable groups:   ,,,,,   ,,,   ,,   ,,,,,   ,,,,   ,   ,   ,,   ,   ,
Allowed substitution hints:   (,,,,,)   (,,,,,,)   (,,,,,)   (,,,,,)   (,,,,,,)   (,,,,,)   (,)   (,,,,,,)   (,,,,,,)   (,,,)   (,)   (,,,,)   (,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)

Proof of Theorem bnj1018
StepHypRef Expression
1 df-bnj17 29444 . . 3
2 bnj258 29465 . . . . . . . 8
3 bnj1018.29 . . . . . . . 8
42, 3sylbir 216 . . . . . . 7
54ex 435 . . . . . 6
65eximdv 1758 . . . . 5
7 bnj1018.3 . . . . . 6
8 bnj1018.9 . . . . . 6
9 bnj1018.12 . . . . . 6
10 bnj1018.14 . . . . . 6
11 bnj1018.16 . . . . . 6
127, 8, 9, 10, 11bnj985 29716 . . . . 5
136, 12syl6ibr 230 . . . 4
1413imp 430 . . 3
151, 14sylbi 198 . 2
16 bnj1019 29543 . . 3
17 bnj1018.30 . . . . . 6
1817simp3d 1019 . . . . 5
19 bnj1018.26 . . . . . . 7
2019bnj1235 29568 . . . . . 6
21 fndm 5636 . . . . . 6
223, 20, 213syl 18 . . . . 5
2318, 22eleqtrrd 2509 . . . 4
2423exlimiv 1770 . . 3
2516, 24sylbir 216 . 2
26 bnj1018.1 . . 3
27 bnj1018.2 . . 3
28 bnj1018.13 . . 3
2911bnj918 29529 . . 3
30 vex 3025 . . . 4
3130sucex 6596 . . 3
3226, 27, 28, 10, 29, 31bnj1015 29724 . 2
3315, 25, 32syl2anc 665 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872  cab 2414  wral 2714  wrex 2715  cvv 3022  wsbc 3242   cdif 3376   cun 3377   wss 3379  c0 3704  csn 3941  cop 3947  ciun 4242   cdm 4796   csuc 5387   wfn 5539  cfv 5544  com 6650   w-bnj17 29443   c-bnj14 29445   w-bnj15 29449   c-bnj18 29451 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-pr 4603  ax-un 6541 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-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-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-iun 4244  df-br 4367  df-dm 4806  df-suc 5391  df-iota 5508  df-fn 5547  df-fv 5552  df-bnj17 29444  df-bnj18 29452 This theorem is referenced by:  bnj1020  29726
 Copyright terms: Public domain W3C validator