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

Theorem bnj969 28963
 Description: Technical lemma for bnj69 29025. 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
bnj969.1
bnj969.2
bnj969.3
bnj969.10
bnj969.12
bnj969.14
bnj969.15
Assertion
Ref Expression
bnj969
Distinct variable groups:   ,,,   ,,,   ,,,   ,,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   (,,)   (,,,,,)   (,,,,,)   (,,)   (,,,,,)

Proof of Theorem bnj969
StepHypRef Expression
1 simpl 444 . . . 4
2 bnj667 28766 . . . . . . 7
3 bnj969.3 . . . . . . 7
4 bnj969.14 . . . . . . 7
52, 3, 43imtr4i 258 . . . . . 6
653ad2ant1 978 . . . . 5
76adantl 453 . . . 4
83bnj1232 28821 . . . . . . 7
9 vex 2916 . . . . . . . 8
109bnj216 28745 . . . . . . 7
11 id 20 . . . . . . 7
128, 10, 113anim123i 1139 . . . . . 6
13 bnj969.15 . . . . . . 7
14 3ancomb 945 . . . . . . 7
1513, 14bitri 241 . . . . . 6
1612, 15sylibr 204 . . . . 5
1716adantl 453 . . . 4
181, 7, 17jca32 522 . . 3
19 bnj256 28716 . . 3
2018, 19sylibr 204 . 2
21 bnj969.12 . . 3
22 bnj969.10 . . . 4
23 bnj969.1 . . . 4
24 bnj969.2 . . . 4
2522, 4, 13, 23, 24bnj938 28954 . . 3
2621, 25syl5eqel 2485 . 2
2720, 26syl 16 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721  wral 2663  cvv 2913   cdif 3274  c0 3585  csn 3771  ciun 4049   csuc 4538  com 4799   wfn 5403  cfv 5408   w-bnj17 28696   c-bnj14 28698   w-bnj15 28702 This theorem is referenced by:  bnj910  28965  bnj1006  28976 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-rep 4275  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-reu 2670  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  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-mpt 4223  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-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-bnj17 28697  df-bnj14 28699  df-bnj13 28701  df-bnj15 28703
 Copyright terms: Public domain W3C validator