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

Theorem bnj594 29723
 Description: Technical lemma for bnj852 29732. 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
bnj594.1
bnj594.2
bnj594.3
bnj594.7
bnj594.9
bnj594.10
bnj594.11
bnj594.15
bnj594.16
bnj594.17
Assertion
Ref Expression
bnj594
Distinct variable groups:   ,,   ,   ,,   ,   ,   ,,,   ,,,   ,,   ,
Allowed substitution hints:   (,,,,,,,)   (,,,,,,,)   (,,,,,,)   (,,,,,,,)   (,,,,,,,)   (,,,,,)   (,,,,,,)   (,,,,,)   (,,,,,,,)   (,,,,,,,)   (,,,,,,)

Proof of Theorem bnj594
StepHypRef Expression
1 bnj594.3 . . . . . . . . 9
21simp2bi 1024 . . . . . . . 8
3 bnj594.1 . . . . . . . 8
42, 3sylib 200 . . . . . . 7
5 bnj594.11 . . . . . . . . 9
65simp2bi 1024 . . . . . . . 8
7 bnj594.9 . . . . . . . 8
86, 7sylib 200 . . . . . . 7
9 eqtr3 2472 . . . . . . 7
104, 8, 9syl2an 480 . . . . . 6
11103adant1 1026 . . . . 5
12 fveq2 5865 . . . . . 6
13 fveq2 5865 . . . . . 6
1412, 13eqeq12d 2466 . . . . 5
1511, 14syl5ibr 225 . . . 4
16 bnj594.15 . . . 4
1715, 16sylibr 216 . . 3
1817a1d 26 . 2
19 bnj253 29509 . . . . . 6
20 bnj252 29508 . . . . . 6
21 anidm 650 . . . . . . 7
22213anbi1i 1199 . . . . . 6
2319, 20, 223bitr3i 279 . . . . 5
24 df-bnj17 29492 . . . . . . . . . 10
25 bnj594.17 . . . . . . . . . . . 12
2625bnj1095 29593 . . . . . . . . . . 11
2726bnj1352 29639 . . . . . . . . . 10
2824, 27hbxfrbi 1694 . . . . . . . . 9
29 bnj170 29503 . . . . . . . . . . . 12
30 bnj594.7 . . . . . . . . . . . . . . 15
3130bnj923 29579 . . . . . . . . . . . . . 14
32 elnn 6702 . . . . . . . . . . . . . 14
3331, 32sylan2 477 . . . . . . . . . . . . 13
3433anim1i 572 . . . . . . . . . . . 12
3529, 34sylbi 199 . . . . . . . . . . 11
36 nnsuc 6709 . . . . . . . . . . 11
37 rexex 2844 . . . . . . . . . . 11
3835, 36, 373syl 18 . . . . . . . . . 10
3938bnj721 29567 . . . . . . . . 9
4028, 39bnj596 29556 . . . . . . . 8
41 bnj667 29562 . . . . . . . . . . 11
4241anim1i 572 . . . . . . . . . 10
43 bnj258 29513 . . . . . . . . . 10
4442, 43sylibr 216 . . . . . . . . 9
45 df-bnj17 29492 . . . . . . . . . . . . . . 15
46 bnj219 29541 . . . . . . . . . . . . . . . . . 18
47463ad2ant3 1031 . . . . . . . . . . . . . . . . 17
4847adantr 467 . . . . . . . . . . . . . . . 16
49 vex 3048 . . . . . . . . . . . . . . . . . . 19
5049bnj216 29540 . . . . . . . . . . . . . . . . . 18
51 df-3an 987 . . . . . . . . . . . . . . . . . . . 20
52 3anrot 990 . . . . . . . . . . . . . . . . . . . 20
53 ancom 452 . . . . . . . . . . . . . . . . . . . 20
5451, 52, 533bitr3i 279 . . . . . . . . . . . . . . . . . . 19
55 eldifi 3555 . . . . . . . . . . . . . . . . . . . . . 22
5655, 30eleq2s 2547 . . . . . . . . . . . . . . . . . . . . 21
57 nnord 6700 . . . . . . . . . . . . . . . . . . . . 21
58 ordtr1 5466 . . . . . . . . . . . . . . . . . . . . 21
5956, 57, 583syl 18 . . . . . . . . . . . . . . . . . . . 20
6059imp 431 . . . . . . . . . . . . . . . . . . 19
6154, 60sylbi 199 . . . . . . . . . . . . . . . . . 18
6250, 61syl3an3 1303 . . . . . . . . . . . . . . . . 17
63 rsp 2754 . . . . . . . . . . . . . . . . . 18
6425, 63sylbi 199 . . . . . . . . . . . . . . . . 17
6562, 64mpan9 472 . . . . . . . . . . . . . . . 16
6648, 65mpd 15 . . . . . . . . . . . . . . 15
6745, 66sylbi 199 . . . . . . . . . . . . . 14
6867anim1i 572 . . . . . . . . . . . . 13
69 bnj252 29508 . . . . . . . . . . . . 13
7068, 69sylibr 216 . . . . . . . . . . . 12
71 bnj446 29522 . . . . . . . . . . . . 13
72 bnj594.16 . . . . . . . . . . . . . 14
73 pm3.35 591 . . . . . . . . . . . . . 14
7472, 73sylan2b 478 . . . . . . . . . . . . 13
7571, 74sylbi 199 . . . . . . . . . . . 12
76 iuneq1 4292 . . . . . . . . . . . 12
7770, 75, 763syl 18 . . . . . . . . . . 11
78 bnj658 29561 . . . . . . . . . . . . 13
791simp3bi 1025 . . . . . . . . . . . . . 14
805simp3bi 1025 . . . . . . . . . . . . . 14
8179, 80bnj240 29504 . . . . . . . . . . . . 13
8278, 81anim12i 570 . . . . . . . . . . . 12
83 simpl 459 . . . . . . . . . . . . 13
8483anim2i 573 . . . . . . . . . . . 12
85 simp3 1010 . . . . . . . . . . . . . 14
8685anim1i 572 . . . . . . . . . . . . 13
87 simpl1 1011 . . . . . . . . . . . . . 14
88 df-3an 987 . . . . . . . . . . . . . . . . 17
89 ancom 452 . . . . . . . . . . . . . . . . 17
9088, 89bitri 253 . . . . . . . . . . . . . . . 16
91 elnn 6702 . . . . . . . . . . . . . . . . 17
9250, 33, 91syl2an 480 . . . . . . . . . . . . . . . 16
9390, 92sylbi 199 . . . . . . . . . . . . . . 15
94 bnj594.2 . . . . . . . . . . . . . . . . 17
9594bnj589 29720 . . . . . . . . . . . . . . . 16
9695bnj590 29721 . . . . . . . . . . . . . . 15
9793, 96mpan9 472 . . . . . . . . . . . . . 14
9887, 97mpd 15 . . . . . . . . . . . . 13
9986, 98syldan 473 . . . . . . . . . . . 12
10082, 84, 993syl 18 . . . . . . . . . . 11
101 simpr 463 . . . . . . . . . . . . 13
102101anim2i 573 . . . . . . . . . . . 12
10385anim1i 572 . . . . . . . . . . . . 13
104 simpl1 1011 . . . . . . . . . . . . . 14
105 bnj594.10 . . . . . . . . . . . . . . . . 17
106105bnj589 29720 . . . . . . . . . . . . . . . 16
107106bnj590 29721 . . . . . . . . . . . . . . 15
10893, 107mpan9 472 . . . . . . . . . . . . . 14
109104, 108mpd 15 . . . . . . . . . . . . 13
110103, 109syldan 473 . . . . . . . . . . . 12
11182, 102, 1103syl 18 . . . . . . . . . . 11
11277, 100, 1113eqtr4d 2495 . . . . . . . . . 10
113112ex 436 . . . . . . . . 9
11444, 113syl 17 . . . . . . . 8
11540, 114bnj593 29555 . . . . . . 7
116 bnj258 29513 . . . . . . 7
117 19.9v 1812 . . . . . . 7
118115, 116, 1173imtr3i 269 . . . . . 6
119118expimpd 608 . . . . 5
12023, 119syl5bir 222 . . . 4
121120, 16sylibr 216 . . 3
1221213expib 1211 . 2
12318, 122pm2.61ine 2707 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 985   wceq 1444  wex 1663   wcel 1887   wne 2622  wral 2737  wrex 2738  wsbc 3267   cdif 3401  c0 3731  csn 3968  ciun 4278   class class class wbr 4402   cep 4743   word 5422   csuc 5425   wfn 5577  cfv 5582  com 6692   w-bnj17 29491   c-bnj14 29493 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-tr 4498  df-eprel 4745  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fv 5590  df-om 6693  df-bnj17 29492 This theorem is referenced by:  bnj580  29724
 Copyright terms: Public domain W3C validator