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

Theorem bnj1145 29424
 Description: Technical lemma for bnj69 29441. 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
bnj1145.1
bnj1145.2
bnj1145.3
bnj1145.4
bnj1145.5
bnj1145.6
Assertion
Ref Expression
bnj1145
Distinct variable groups:   ,,,,,   ,,   ,,,,,   ,,,,   ,   ,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,)   ()

Proof of Theorem bnj1145
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1145.1 . . 3
2 bnj1145.2 . . 3
3 bnj1145.3 . . 3
4 bnj1145.4 . . 3
51, 2, 3, 4bnj882 29359 . 2
6 ss2iun 4110 . . . 4
7 bnj1145.5 . . . . . . 7
87, 4bnj1083 29409 . . . . . 6
92bnj1095 29214 . . . . . . . . . 10
109, 7bnj1096 29215 . . . . . . . . 9
1110nfi 1561 . . . . . . . 8
123bnj1098 29216 . . . . . . . . . . . . . . . . 17
137bnj1232 29237 . . . . . . . . . . . . . . . . . 18
14133anim3i 1142 . . . . . . . . . . . . . . . . 17
1512, 14bnj1101 29217 . . . . . . . . . . . . . . . 16
16 ancl 531 . . . . . . . . . . . . . . . 16
1715, 16bnj101 29150 . . . . . . . . . . . . . . 15
18 bnj1145.6 . . . . . . . . . . . . . . . . 17
1918imbi2i 305 . . . . . . . . . . . . . . . 16
2019exbii 1593 . . . . . . . . . . . . . . 15
2117, 20mpbir 202 . . . . . . . . . . . . . 14
22 bnj213 29315 . . . . . . . . . . . . . . . 16
2322bnj226 29163 . . . . . . . . . . . . . . 15
24 simpr 449 . . . . . . . . . . . . . . . . . . 19
2518, 24bnj833 29189 . . . . . . . . . . . . . . . . . 18
26 simp2 959 . . . . . . . . . . . . . . . . . . . 20
27133ad2ant3 981 . . . . . . . . . . . . . . . . . . . 20
283bnj923 29199 . . . . . . . . . . . . . . . . . . . . 21
29 elnn 4857 . . . . . . . . . . . . . . . . . . . . 21
3028, 29sylan2 462 . . . . . . . . . . . . . . . . . . . 20
3126, 27, 30syl2anc 644 . . . . . . . . . . . . . . . . . . 19
3218, 31bnj832 29188 . . . . . . . . . . . . . . . . . 18
33 vex 2961 . . . . . . . . . . . . . . . . . . . 20
3433bnj216 29161 . . . . . . . . . . . . . . . . . . 19
35 elnn 4857 . . . . . . . . . . . . . . . . . . 19
3634, 35sylan 459 . . . . . . . . . . . . . . . . . 18
3725, 32, 36syl2anc 644 . . . . . . . . . . . . . . . . 17
3818, 26bnj832 29188 . . . . . . . . . . . . . . . . . 18
3925, 38eqeltrrd 2513 . . . . . . . . . . . . . . . . 17
402bnj589 29342 . . . . . . . . . . . . . . . . . . . . . . 23
4140biimpi 188 . . . . . . . . . . . . . . . . . . . . . 22
4241bnj708 29186 . . . . . . . . . . . . . . . . . . . . 21
43 rsp 2768 . . . . . . . . . . . . . . . . . . . . 21
4442, 43syl 16 . . . . . . . . . . . . . . . . . . . 20
457, 44sylbi 189 . . . . . . . . . . . . . . . . . . 19
46453ad2ant3 981 . . . . . . . . . . . . . . . . . 18
4718, 46bnj832 29188 . . . . . . . . . . . . . . . . 17
4837, 39, 47mp2d 44 . . . . . . . . . . . . . . . 16
49 fveq2 5730 . . . . . . . . . . . . . . . . . 18
5049eqeq1d 2446 . . . . . . . . . . . . . . . . 17
5125, 50syl 16 . . . . . . . . . . . . . . . 16
5248, 51mpbird 225 . . . . . . . . . . . . . . 15
5323, 52bnj1262 29244 . . . . . . . . . . . . . 14
5421, 53bnj1023 29213 . . . . . . . . . . . . 13
55 3anass 941 . . . . . . . . . . . . . . 15
5655imbi1i 317 . . . . . . . . . . . . . 14
5756exbii 1593 . . . . . . . . . . . . 13
5854, 57mpbi 201 . . . . . . . . . . . 12
591biimpi 188 . . . . . . . . . . . . . . 15
607, 59bnj771 29195 . . . . . . . . . . . . . 14
61 fveq2 5730 . . . . . . . . . . . . . . 15
62 bnj213 29315 . . . . . . . . . . . . . . . 16
63 sseq1 3371 . . . . . . . . . . . . . . . 16
6462, 63mpbiri 226 . . . . . . . . . . . . . . 15
65 sseq1 3371 . . . . . . . . . . . . . . . 16
6665biimpar 473 . . . . . . . . . . . . . . 15
6761, 64, 66syl2an 465 . . . . . . . . . . . . . 14
6860, 67sylan2 462 . . . . . . . . . . . . 13
6968adantrl 698 . . . . . . . . . . . 12
7058, 69bnj1109 29219 . . . . . . . . . . 11
71 19.9v 1677 . . . . . . . . . . 11
7270, 71mpbi 201 . . . . . . . . . 10
7372expcom 426 . . . . . . . . 9
74 fndm 5546 . . . . . . . . . . 11
757, 74bnj770 29194 . . . . . . . . . 10
76 eleq2 2499 . . . . . . . . . . 11
7776imbi1d 310 . . . . . . . . . 10
7875, 77syl 16 . . . . . . . . 9
7973, 78mpbird 225 . . . . . . . 8
8011, 79ralrimi 2789 . . . . . . 7
8180exlimiv 1645 . . . . . 6
828, 81sylbi 189 . . . . 5
83 ss2iun 4110 . . . . . 6
84 bnj1143 29223 . . . . . 6
8583, 84syl6ss 3362 . . . . 5
8682, 85syl 16 . . . 4
876, 86mprg 2777 . . 3
884bnj1317 29255 . . . 4
8988bnj1146 29224 . . 3
9087, 89sstri 3359 . 2
915, 90eqsstri 3380 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726  cab 2424   wne 2601  wral 2707  wrex 2708   cdif 3319   wss 3322  c0 3630  csn 3816  ciun 4095   csuc 4585  com 4847   cdm 4880   wfn 5451  cfv 5456   w-bnj17 29112   c-bnj14 29114   c-bnj18 29120 This theorem is referenced by:  bnj1147  29425 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405  ax-un 4703 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-tr 4305  df-eprel 4496  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-iota 5420  df-fn 5459  df-fv 5464  df-bnj17 29113  df-bnj14 29115  df-bnj18 29121
 Copyright terms: Public domain W3C validator