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

Theorem bnj571 33671
 Description: Technical lemma for bnj852 33686. 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
bnj571.3
bnj571.16
bnj571.17
bnj571.18
bnj571.19
bnj571.20
bnj571.22
bnj571.23
bnj571.24
bnj571.25
bnj571.26
bnj571.29
bnj571.30
bnj571.38
bnj571.21
bnj571.40
bnj571.33
Assertion
Ref Expression
bnj571
Distinct variable groups:   ,,,   ,   ,,,   ,   ,,,   ,,   ,,
Allowed substitution hints:   (,,,,,,)   (,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,)   (,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,)   (,,,,,,)   (,,,,,,)

Proof of Theorem bnj571
StepHypRef Expression
1 nfv 1692 . . . 4
2 bnj571.17 . . . . 5
3 nfv 1692 . . . . . 6
4 nfv 1692 . . . . . 6
5 bnj571.30 . . . . . . 7
6 nfra1 2822 . . . . . . 7
75, 6nfxfr 1630 . . . . . 6
83, 4, 7nf3an 1914 . . . . 5
92, 8nfxfr 1630 . . . 4
10 nfv 1692 . . . 4
111, 9, 10nf3an 1914 . . 3
12 df-bnj17 33447 . . . . . . . . 9
13 3anass 976 . . . . . . . . . 10
14 3anrot 977 . . . . . . . . . 10
15 bnj571.20 . . . . . . . . . . . 12
16 df-3an 974 . . . . . . . . . . . 12
1715, 16bitri 249 . . . . . . . . . . 11
1817anbi2i 694 . . . . . . . . . 10
1913, 14, 183bitr4ri 278 . . . . . . . . 9
2012, 19bitri 249 . . . . . . . 8
21 bnj571.3 . . . . . . . . 9
22 bnj571.16 . . . . . . . . 9
23 bnj571.18 . . . . . . . . 9
24 bnj571.19 . . . . . . . . 9
25 bnj571.22 . . . . . . . . 9
26 bnj571.23 . . . . . . . . 9
27 bnj571.24 . . . . . . . . 9
28 bnj571.25 . . . . . . . . 9
29 bnj571.26 . . . . . . . . 9
30 bnj571.29 . . . . . . . . 9
31 bnj571.38 . . . . . . . . 9
3221, 22, 2, 23, 24, 15, 25, 26, 27, 28, 29, 30, 5, 31bnj558 33667 . . . . . . . 8
3320, 32sylbir 213 . . . . . . 7
34333expib 1198 . . . . . 6
35 df-bnj17 33447 . . . . . . . . 9
36 3anass 976 . . . . . . . . . 10
37 3anrot 977 . . . . . . . . . 10
38 bnj571.21 . . . . . . . . . . . 12
39 df-3an 974 . . . . . . . . . . . 12
4038, 39bitri 249 . . . . . . . . . . 11
4140anbi2i 694 . . . . . . . . . 10
4236, 37, 413bitr4ri 278 . . . . . . . . 9
4335, 42bitri 249 . . . . . . . 8
44 bnj571.40 . . . . . . . . 9
4521, 2, 24, 38, 27, 22, 44, 5bnj570 33670 . . . . . . . 8
4643, 45sylbir 213 . . . . . . 7
47463expib 1198 . . . . . 6
4834, 47pm2.61ine 2754 . . . . 5
4948, 27syl6eq 2498 . . . 4
5049exp32 605 . . 3
5111, 50alrimi 1861 . 2
52 bnj571.33 . . 3
5352bnj946 33540 . 2
5451, 53sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 972  wal 1379   wceq 1381   wcel 1802   wne 2636  wral 2791   cdif 3455   cun 3456  c0 3767  csn 4010  cop 4016  ciun 4311   csuc 4866   wfn 5569  cfv 5574  com 6681   w-bnj17 33446   c-bnj14 33448   w-bnj15 33452 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672  ax-un 6573  ax-reg 8016 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-res 4997  df-iota 5537  df-fun 5576  df-fn 5577  df-fv 5582  df-om 6682  df-bnj17 33447 This theorem is referenced by:  bnj600  33684  bnj908  33696
 Copyright terms: Public domain W3C validator