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

Theorem bnj1128 28782
 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
bnj1128.1
bnj1128.2
bnj1128.3
bnj1128.4
bnj1128.5
bnj1128.6
bnj1128.7
bnj1128.8
bnj1128.9
bnj1128.10
bnj1128.11
Assertion
Ref Expression
bnj1128
Distinct variable groups:   ,,,,,   ,,,   ,,,,,   ,,,,   ,,,,   ,   ,,   ,
Allowed substitution hints:   (,,)   (,,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)   (,)   ()   ()   (,,,,)   (,,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1128
StepHypRef Expression
1 bnj1128.1 . . . 4
2 bnj1128.2 . . . 4
3 bnj1128.3 . . . 4
4 bnj1128.4 . . . 4
5 bnj1128.5 . . . 4
61, 2, 3, 4, 5bnj981 28744 . . 3
7 simp1 955 . . . . . 6
8 simp2 956 . . . . . 6
9 bnj1128.7 . . . . . . . . 9
10 nfv 1619 . . . . . . . . . . . . . . 15
11 nfra1 2669 . . . . . . . . . . . . . . . 16
129, 11nfxfr 1570 . . . . . . . . . . . . . . 15
13 nfv 1619 . . . . . . . . . . . . . . 15
1410, 12, 13nf3an 1832 . . . . . . . . . . . . . 14
15 nfv 1619 . . . . . . . . . . . . . 14
1614, 15nfim 1815 . . . . . . . . . . . . 13
1716nfri 1763 . . . . . . . . . . . 12
183bnj1098 28577 . . . . . . . . . . . . . . . . 17
19 simpl 443 . . . . . . . . . . . . . . . . . 18
20 simpr1 961 . . . . . . . . . . . . . . . . . 18
215bnj1232 28598 . . . . . . . . . . . . . . . . . . . 20
22213ad2ant3 978 . . . . . . . . . . . . . . . . . . 19
2322adantl 452 . . . . . . . . . . . . . . . . . 18
2419, 20, 233jca 1132 . . . . . . . . . . . . . . . . 17
2518, 24bnj1101 28578 . . . . . . . . . . . . . . . 16
26 ancl 529 . . . . . . . . . . . . . . . 16
2725, 26bnj101 28511 . . . . . . . . . . . . . . 15
28 df-3an 936 . . . . . . . . . . . . . . . . 17
2928imbi2i 303 . . . . . . . . . . . . . . . 16
3029exbii 1582 . . . . . . . . . . . . . . 15
3127, 30mpbir 200 . . . . . . . . . . . . . 14
32 bnj213 28676 . . . . . . . . . . . . . . . 16
3332bnj226 28524 . . . . . . . . . . . . . . 15
34 simp21 988 . . . . . . . . . . . . . . . 16
35 simp3r 984 . . . . . . . . . . . . . . . . 17
36 biid 227 . . . . . . . . . . . . . . . . . . . . . 22
37 biid 227 . . . . . . . . . . . . . . . . . . . . . 22
38 bnj1128.8 . . . . . . . . . . . . . . . . . . . . . . 23
39 vex 2867 . . . . . . . . . . . . . . . . . . . . . . . 24
40 nfv 1619 . . . . . . . . . . . . . . . . . . . . . . . . 25
4140sbcgf 3130 . . . . . . . . . . . . . . . . . . . . . . . 24
4239, 41ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23
4338, 42bitr2i 241 . . . . . . . . . . . . . . . . . . . . . 22
44 bnj1128.9 . . . . . . . . . . . . . . . . . . . . . . . 24
452, 44bnj1039 28763 . . . . . . . . . . . . . . . . . . . . . . 23
462, 45bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22
4736, 37, 43, 46bnj887 28557 . . . . . . . . . . . . . . . . . . . . 21
48 bnj1128.10 . . . . . . . . . . . . . . . . . . . . . 22
4938, 44, 5, 48bnj1040 28764 . . . . . . . . . . . . . . . . . . . . 21
5047, 5, 493bitr4i 268 . . . . . . . . . . . . . . . . . . . 20
5149bnj1254 28604 . . . . . . . . . . . . . . . . . . . 20
5250, 51sylbi 187 . . . . . . . . . . . . . . . . . . 19
53523ad2ant3 978 . . . . . . . . . . . . . . . . . 18
54533ad2ant2 977 . . . . . . . . . . . . . . . . 17
55 simp3l 983 . . . . . . . . . . . . . . . . . 18
56223ad2ant2 977 . . . . . . . . . . . . . . . . . 18
573bnj923 28560 . . . . . . . . . . . . . . . . . . 19
58 elnn 4748 . . . . . . . . . . . . . . . . . . 19
5957, 58sylan2 460 . . . . . . . . . . . . . . . . . 18
6055, 56, 59syl2anc 642 . . . . . . . . . . . . . . . . 17
6145bnj589 28703 . . . . . . . . . . . . . . . . . . 19
62 rsp 2679 . . . . . . . . . . . . . . . . . . 19
6361, 62sylbi 187 . . . . . . . . . . . . . . . . . 18
64 eleq1 2418 . . . . . . . . . . . . . . . . . . . 20
65 fveq2 5608 . . . . . . . . . . . . . . . . . . . . 21
6665eqeq1d 2366 . . . . . . . . . . . . . . . . . . . 20
6764, 66imbi12d 311 . . . . . . . . . . . . . . . . . . 19
6867imbi2d 307 . . . . . . . . . . . . . . . . . 18
6963, 68syl5ibr 212 . . . . . . . . . . . . . . . . 17
7035, 54, 60, 69syl3c 57 . . . . . . . . . . . . . . . 16
7134, 70mpd 14 . . . . . . . . . . . . . . 15
7233, 71bnj1262 28605 . . . . . . . . . . . . . 14
7331, 72bnj1023 28574 . . . . . . . . . . . . 13
745bnj1247 28603 . . . . . . . . . . . . . . 15
75743ad2ant3 978 . . . . . . . . . . . . . 14
76 bnj213 28676 . . . . . . . . . . . . . . 15
77 fveq2 5608 . . . . . . . . . . . . . . . 16
781biimpi 186 . . . . . . . . . . . . . . . 16
7977, 78sylan9eq 2410 . . . . . . . . . . . . . . 15
8076, 79bnj1262 28605 . . . . . . . . . . . . . 14
8175, 80sylan2 460 . . . . . . . . . . . . 13
8273, 81bnj1109 28580 . . . . . . . . . . . 12
8317, 82bnj1131 28581 . . . . . . . . . . 11
84833expia 1153 . . . . . . . . . 10
85 bnj1128.6 . . . . . . . . . 10
8684, 85sylibr 203 . . . . . . . . 9
873, 5, 9, 86bnj1133 28781 . . . . . . . 8
8885ralbii 2643 . . . . . . . 8
8987, 88sylib 188 . . . . . . 7
90 rsp 2679 . . . . . . 7
9189, 90syl 15 . . . . . 6
927, 8, 7, 91syl3c 57 . . . . 5
93 simp3 957 . . . . 5
9492, 93sseldd 3257 . . . 4
95942eximi 1577 . . 3
966, 95bnj593 28536 . 2
97 19.9v 1664 . . 3
98 19.9v 1664 . . 3
99 19.9v 1664 . . 3
10097, 98, 993bitri 262 . 2
10196, 100sylib 188 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  cvv 2864  wsbc 3067   cdif 3225   wss 3228  c0 3531  csn 3716  ciun 3986   class class class wbr 4104   cep 4385   csuc 4476  com 4738   wfn 5332  cfv 5337   w-bnj17 28473   c-bnj14 28475   c-bnj18 28481 This theorem is referenced by:  bnj1127  28783 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-csb 3158  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