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

Theorem bnj570 29709
 Description: Technical lemma for bnj852 29725. 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 29500 . . . 4
2 bnj570.17 . . . . . 6
32simp3bi 1024 . . . . 5
4 bnj570.21 . . . . . . . 8
54simp1bi 1022 . . . . . . 7
65adantl 468 . . . . . 6
7 bnj570.19 . . . . . . 7
87, 4bnj563 29546 . . . . . 6
96, 8jca 535 . . . . 5
10 bnj570.30 . . . . . . . 8
1110bnj946 29579 . . . . . . 7
12 sp 1936 . . . . . . 7
1311, 12sylbi 199 . . . . . 6
1413imp32 435 . . . . 5
153, 9, 14syl2an 480 . . . 4
161, 15bnj833 29562 . . 3
17 bnj570.40 . . . . . 6
1817bnj930 29574 . . . . 5
1918bnj721 29560 . . . 4
20 bnj570.26 . . . . . 6
2120bnj931 29575 . . . . 5
2221a1i 11 . . . 4
23 bnj667 29555 . . . . 5
242bnj564 29547 . . . . . . 7
25 eleq2 2517 . . . . . . . 8
2625biimpar 488 . . . . . . 7
2724, 8, 26syl2an 480 . . . . . 6
28273impb 1203 . . . . 5
2923, 28syl 17 . . . 4
3019, 22, 29bnj1502 29652 . . 3
312simp1bi 1022 . . . . . . . . 9
32 bnj252 29501 . . . . . . . . . . . . . 14
3332simplbi 462 . . . . . . . . . . . . 13
347, 33sylbi 199 . . . . . . . . . . . 12
35 eldifi 3554 . . . . . . . . . . . . 13
36 bnj570.3 . . . . . . . . . . . . 13
3735, 36eleq2s 2546 . . . . . . . . . . . 12
38 nnord 6697 . . . . . . . . . . . 12
3934, 37, 383syl 18 . . . . . . . . . . 11
4039adantr 467 . . . . . . . . . 10
4140, 8jca 535 . . . . . . . . 9
4231, 41anim12i 569 . . . . . . . 8
43 fndm 5673 . . . . . . . . 9
44 elelsuc 5494 . . . . . . . . . 10
45 ordsucelsuc 6646 . . . . . . . . . . 11
4645biimpar 488 . . . . . . . . . 10
4744, 46sylan2 477 . . . . . . . . 9
4843, 47anim12i 569 . . . . . . . 8
49 eleq2 2517 . . . . . . . . 9
5049biimpar 488 . . . . . . . 8
5142, 48, 503syl 18 . . . . . . 7
52513impb 1203 . . . . . 6
5323, 52syl 17 . . . . 5
5419, 22, 53bnj1502 29652 . . . 4
5554iuneq1d 4302 . . 3
5616, 30, 553eqtr4d 2494 . 2
57 bnj570.24 . 2
5856, 57syl6eqr 2502 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 984  wal 1441   wceq 1443   wcel 1886   wne 2621  wral 2736   cdif 3400   cun 3401   wss 3403  c0 3730  csn 3967  cop 3973  ciun 4277   cdm 4833   word 5421   csuc 5424   wfun 5575   wfn 5576  cfv 5581  com 6689   w-bnj17 29484   c-bnj14 29486   w-bnj15 29490 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-res 4845  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-fv 5589  df-om 6690  df-bnj17 29485 This theorem is referenced by:  bnj571  29710
 Copyright terms: Public domain W3C validator