Mathbox for Jeff Hankins < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filnetlem3 Unicode version

Theorem filnetlem3 26329
 Description: Lemma for filnet 26331. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
filnet.h
filnet.d
Assertion
Ref Expression
filnetlem3
Distinct variable groups:   ,,,   ,,   ,
Allowed substitution hints:   (,,)   ()   (,)

Proof of Theorem filnetlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmresi 5005 . . . . . 6
2 filnet.h . . . . . . . . 9
3 filnet.d . . . . . . . . 9
42, 3filnetlem2 26328 . . . . . . . 8
54simpli 444 . . . . . . 7
6 dmss 4878 . . . . . . 7
75, 6ax-mp 8 . . . . . 6
81, 7eqsstr3i 3209 . . . . 5
9 ssun1 3338 . . . . 5
108, 9sstri 3188 . . . 4
11 dmrnssfld 4938 . . . 4
1210, 11sstri 3188 . . 3
134simpri 448 . . . . 5
14 uniss 3848 . . . . 5
15 uniss 3848 . . . . 5
1613, 14, 15mp2b 9 . . . 4
17 unixpss 4799 . . . . 5
18 unidm 3318 . . . . 5
1917, 18sseqtri 3210 . . . 4
2016, 19sstri 3188 . . 3
2112, 20eqssi 3195 . 2
22 filelss 17547 . . . . . . . 8
23 xpss2 4796 . . . . . . . 8
2422, 23syl 15 . . . . . . 7
2524ralrimiva 2626 . . . . . 6
26 ss2iun 3920 . . . . . 6
2725, 26syl 15 . . . . 5
28 iunxpconst 4746 . . . . 5
2927, 28syl6sseq 3224 . . . 4
302, 29syl5eqss 3222 . . 3
315a1i 10 . . . . 5
323relopabi 4811 . . . . 5
3331, 32jctil 523 . . . 4
34 simpl 443 . . . . . . . . . 10
3530adantr 451 . . . . . . . . . . . 12
36 simprl 732 . . . . . . . . . . . 12
3735, 36sseldd 3181 . . . . . . . . . . 11
38 xp1st 6149 . . . . . . . . . . 11
3937, 38syl 15 . . . . . . . . . 10
40 simprr 733 . . . . . . . . . . . 12
4135, 40sseldd 3181 . . . . . . . . . . 11
42 xp1st 6149 . . . . . . . . . . 11
4341, 42syl 15 . . . . . . . . . 10
44 filinn0 17555 . . . . . . . . . 10
4534, 39, 43, 44syl3anc 1182 . . . . . . . . 9
46 n0 3464 . . . . . . . . 9
4745, 46sylib 188 . . . . . . . 8
4836adantr 451 . . . . . . . . . . . 12
49 filin 17549 . . . . . . . . . . . . . . . 16
5034, 39, 43, 49syl3anc 1182 . . . . . . . . . . . . . . 15
5150adantr 451 . . . . . . . . . . . . . 14
52 simpr 447 . . . . . . . . . . . . . 14
53 id 19 . . . . . . . . . . . . . . 15
5453opeliunxp2 4824 . . . . . . . . . . . . . 14
5551, 52, 54sylanbrc 645 . . . . . . . . . . . . 13
5655, 2syl6eleqr 2374 . . . . . . . . . . . 12
57 fvex 5539 . . . . . . . . . . . . . . . 16
5857inex1 4155 . . . . . . . . . . . . . . 15
59 vex 2791 . . . . . . . . . . . . . . 15
6058, 59op1st 6128 . . . . . . . . . . . . . 14
61 inss1 3389 . . . . . . . . . . . . . 14
6260, 61eqsstri 3208 . . . . . . . . . . . . 13
63 vex 2791 . . . . . . . . . . . . . 14
64 opex 4237 . . . . . . . . . . . . . 14
652, 3, 63, 64filnetlem1 26327 . . . . . . . . . . . . 13
6662, 65mpbiran2 885 . . . . . . . . . . . 12
6748, 56, 66sylanbrc 645 . . . . . . . . . . 11
6840adantr 451 . . . . . . . . . . . 12
69 inss2 3390 . . . . . . . . . . . . . 14
7060, 69eqsstri 3208 . . . . . . . . . . . . 13
71 vex 2791 . . . . . . . . . . . . . 14
722, 3, 71, 64filnetlem1 26327 . . . . . . . . . . . . 13
7370, 72mpbiran2 885 . . . . . . . . . . . 12
7468, 56, 73sylanbrc 645 . . . . . . . . . . 11
75 breq2 4027 . . . . . . . . . . . . 13
76 breq2 4027 . . . . . . . . . . . . 13
7775, 76anbi12d 691 . . . . . . . . . . . 12
7864, 77spcev 2875 . . . . . . . . . . 11
7967, 74, 78syl2anc 642 . . . . . . . . . 10
8079ex 423 . . . . . . . . 9
8180exlimdv 1664 . . . . . . . 8
8247, 81mpd 14 . . . . . . 7
8382ralrimivva 2635 . . . . . 6
84 codir 5063 . . . . . 6
8583, 84sylibr 203 . . . . 5
86 vex 2791 . . . . . . . . . . . . 13
872, 3, 63, 86filnetlem1 26327 . . . . . . . . . . . 12
8887simplbi 446 . . . . . . . . . . 11
8988simpld 445 . . . . . . . . . 10
902, 3, 86, 71filnetlem1 26327 . . . . . . . . . . . 12
9190simplbi 446 . . . . . . . . . . 11
9291simprd 449 . . . . . . . . . 10
9389, 92anim12i 549 . . . . . . . . 9
9490simprbi 450 . . . . . . . . . 10
9587simprbi 450 . . . . . . . . . 10
9694, 95sylan9ssr 3193 . . . . . . . . 9
972, 3, 63, 71filnetlem1 26327 . . . . . . . . 9
9893, 96, 97sylanbrc 645 . . . . . . . 8
9998ax-gen 1533 . . . . . . 7
10099gen2 1534 . . . . . 6
101 cotr 5055 . . . . . 6
102100, 101mpbir 200 . . . . 5
10385, 102jctil 523 . . . 4
104 filtop 17550 . . . . . . . . 9
105 xpexg 4800 . . . . . . . . 9
106104, 105mpdan 649 . . . . . . . 8
107 ssexg 4160 . . . . . . . 8
10830, 106, 107syl2anc 642 . . . . . . 7
109 xpexg 4800 . . . . . . 7
110108, 108, 109syl2anc 642 . . . . . 6
111 ssexg 4160 . . . . . 6
11213, 110, 111sylancr 644 . . . . 5
11321isdir 14354 . . . . 5
114112, 113syl 15 . . . 4
11533, 103, 114mpbir2and 888 . . 3
11630, 115jca 518 . 2
11721, 116pm3.2i 441 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wal 1527  wex 1528   wceq 1623   wcel 1684   wne 2446  wral 2543  cvv 2788   cun 3150   cin 3151   wss 3152  c0 3455  csn 3640  cop 3643  cuni 3827  ciun 3905   class class class wbr 4023  copab 4076   cid 4304   cxp 4687  ccnv 4688   cdm 4689   crn 4690   cres 4691   ccom 4693   wrel 4694  cfv 5255  c1st 6120  cdir 14350  cfil 17540 This theorem is referenced by:  filnetlem4  26330 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-1st 6122  df-dir 14352  df-fbas 17520  df-fil 17541
 Copyright terms: Public domain W3C validator