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

Theorem bnj570 28922
 Description: Technical lemma for bnj852 28938. 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
bnj570.3
bnj570.17
bnj570.19
bnj570.21
bnj570.24
bnj570.26
bnj570.40
bnj570.30
Assertion
Ref Expression
bnj570
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,)   (,,,,,)   (,,,,,)   (,,,,,)

Proof of Theorem bnj570
StepHypRef Expression
1 bnj251 28712 . . . 4
2 bnj570.17 . . . . . 6
32simp3bi 974 . . . . 5
4 bnj570.21 . . . . . . . 8
54simp1bi 972 . . . . . . 7
65adantl 453 . . . . . 6
7 bnj570.19 . . . . . . 7
87, 4bnj563 28757 . . . . . 6
96, 8jca 519 . . . . 5
10 bnj570.30 . . . . . . . 8
1110bnj946 28791 . . . . . . 7
12 sp 1759 . . . . . . 7
1311, 12sylbi 188 . . . . . 6
1413imp32 423 . . . . 5
153, 9, 14syl2an 464 . . . 4
161, 15bnj833 28773 . . 3
17 bnj570.40 . . . . . 6
1817bnj930 28786 . . . . 5
1918bnj721 28771 . . . 4
20 bnj570.26 . . . . . 6
2120bnj931 28787 . . . . 5
2221a1i 11 . . . 4
23 bnj667 28766 . . . . 5
242bnj564 28758 . . . . . . 7
25 eleq2 2462 . . . . . . . 8
2625biimpar 472 . . . . . . 7
2724, 8, 26syl2an 464 . . . . . 6
28273impb 1149 . . . . 5
2923, 28syl 16 . . . 4
3019, 22, 29bnj1502 28865 . . 3
312simp1bi 972 . . . . . . . . 9
32 bnj252 28713 . . . . . . . . . . . . . 14
3332simplbi 447 . . . . . . . . . . . . 13
347, 33sylbi 188 . . . . . . . . . . . 12
35 eldifi 3426 . . . . . . . . . . . . 13
36 bnj570.3 . . . . . . . . . . . . 13
3735, 36eleq2s 2493 . . . . . . . . . . . 12
38 nnord 4807 . . . . . . . . . . . 12
3934, 37, 383syl 19 . . . . . . . . . . 11
4039adantr 452 . . . . . . . . . 10
4140, 8jca 519 . . . . . . . . 9
4231, 41anim12i 550 . . . . . . . 8
43 fndm 5498 . . . . . . . . 9
44 elelsuc 4608 . . . . . . . . . 10
45 ordsucelsuc 4756 . . . . . . . . . . 11
4645biimpar 472 . . . . . . . . . 10
4744, 46sylan2 461 . . . . . . . . 9
4843, 47anim12i 550 . . . . . . . 8
49 eleq2 2462 . . . . . . . . 9
5049biimpar 472 . . . . . . . 8
5142, 48, 503syl 19 . . . . . . 7
52513impb 1149 . . . . . 6
5323, 52syl 16 . . . . 5
5419, 22, 53bnj1502 28865 . . . 4
5554iuneq1d 4072 . . 3
5616, 30, 553eqtr4d 2443 . 2
57 bnj570.24 . 2
5856, 57syl6eqr 2451 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936  wal 1546   wceq 1649   wcel 1721   wne 2564  wral 2663   cdif 3274   cun 3275   wss 3277  c0 3585  csn 3771  cop 3774  ciun 4049   word 4535   csuc 4538  com 4799   cdm 4832   wfun 5402   wfn 5403  cfv 5408   w-bnj17 28696   c-bnj14 28698   w-bnj15 28702 This theorem is referenced by:  bnj571  28923 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-sbc 3119  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-iun 4051  df-br 4168  df-opab 4222  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-res 4844  df-iota 5372  df-fun 5410  df-fn 5411  df-fv 5416  df-bnj17 28697
 Copyright terms: Public domain W3C validator