Metamath Proof Explorer


Theorem filnetlem3

Description: Lemma for filnet . (Contributed by Jeff Hankins, 13-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

Ref Expression
Hypotheses filnet.h H=nFn×n
filnet.d D=xy|xHyH1sty1stx
Assertion filnetlem3 H=DFFilXHF×XDDirRel

Proof

Step Hyp Ref Expression
1 filnet.h H=nFn×n
2 filnet.d D=xy|xHyH1sty1stx
3 dmresi domIH=H
4 1 2 filnetlem2 IHDDH×H
5 4 simpli IHD
6 dmss IHDdomIHdomD
7 5 6 ax-mp domIHdomD
8 3 7 eqsstrri HdomD
9 ssun1 domDdomDranD
10 8 9 sstri HdomDranD
11 dmrnssfld domDranDD
12 10 11 sstri HD
13 4 simpri DH×H
14 uniss DH×HDH×H
15 uniss DH×HDH×H
16 13 14 15 mp2b DH×H
17 unixpss H×HHH
18 unidm HH=H
19 17 18 sseqtri H×HH
20 16 19 sstri DH
21 12 20 eqssi H=D
22 filelss FFilXnFnX
23 xpss2 nXn×nn×X
24 22 23 syl FFilXnFn×nn×X
25 24 ralrimiva FFilXnFn×nn×X
26 ss2iun nFn×nn×XnFn×nnFn×X
27 25 26 syl FFilXnFn×nnFn×X
28 iunxpconst nFn×X=F×X
29 27 28 sseqtrdi FFilXnFn×nF×X
30 1 29 eqsstrid FFilXHF×X
31 5 a1i FFilXIHD
32 2 relopabiv RelD
33 31 32 jctil FFilXRelDIHD
34 simpl FFilXvHzHFFilX
35 30 adantr FFilXvHzHHF×X
36 simprl FFilXvHzHvH
37 35 36 sseldd FFilXvHzHvF×X
38 xp1st vF×X1stvF
39 37 38 syl FFilXvHzH1stvF
40 simprr FFilXvHzHzH
41 35 40 sseldd FFilXvHzHzF×X
42 xp1st zF×X1stzF
43 41 42 syl FFilXvHzH1stzF
44 filinn0 FFilX1stvF1stzF1stv1stz
45 34 39 43 44 syl3anc FFilXvHzH1stv1stz
46 n0 1stv1stzuu1stv1stz
47 45 46 sylib FFilXvHzHuu1stv1stz
48 36 adantr FFilXvHzHu1stv1stzvH
49 filin FFilX1stvF1stzF1stv1stzF
50 34 39 43 49 syl3anc FFilXvHzH1stv1stzF
51 50 adantr FFilXvHzHu1stv1stz1stv1stzF
52 simpr FFilXvHzHu1stv1stzu1stv1stz
53 id n=1stv1stzn=1stv1stz
54 53 opeliunxp2 1stv1stzunFn×n1stv1stzFu1stv1stz
55 51 52 54 sylanbrc FFilXvHzHu1stv1stz1stv1stzunFn×n
56 55 1 eleqtrrdi FFilXvHzHu1stv1stz1stv1stzuH
57 fvex 1stvV
58 57 inex1 1stv1stzV
59 vex uV
60 58 59 op1st 1st1stv1stzu=1stv1stz
61 inss1 1stv1stz1stv
62 60 61 eqsstri 1st1stv1stzu1stv
63 vex vV
64 opex 1stv1stzuV
65 1 2 63 64 filnetlem1 vD1stv1stzuvH1stv1stzuH1st1stv1stzu1stv
66 62 65 mpbiran2 vD1stv1stzuvH1stv1stzuH
67 48 56 66 sylanbrc FFilXvHzHu1stv1stzvD1stv1stzu
68 40 adantr FFilXvHzHu1stv1stzzH
69 inss2 1stv1stz1stz
70 60 69 eqsstri 1st1stv1stzu1stz
71 vex zV
72 1 2 71 64 filnetlem1 zD1stv1stzuzH1stv1stzuH1st1stv1stzu1stz
73 70 72 mpbiran2 zD1stv1stzuzH1stv1stzuH
74 68 56 73 sylanbrc FFilXvHzHu1stv1stzzD1stv1stzu
75 breq2 w=1stv1stzuvDwvD1stv1stzu
76 breq2 w=1stv1stzuzDwzD1stv1stzu
77 75 76 anbi12d w=1stv1stzuvDwzDwvD1stv1stzuzD1stv1stzu
78 64 77 spcev vD1stv1stzuzD1stv1stzuwvDwzDw
79 67 74 78 syl2anc FFilXvHzHu1stv1stzwvDwzDw
80 47 79 exlimddv FFilXvHzHwvDwzDw
81 80 ralrimivva FFilXvHzHwvDwzDw
82 codir H×HD-1DvHzHwvDwzDw
83 81 82 sylibr FFilXH×HD-1D
84 vex wV
85 1 2 63 84 filnetlem1 vDwvHwH1stw1stv
86 85 simplbi vDwvHwH
87 86 simpld vDwvH
88 1 2 84 71 filnetlem1 wDzwHzH1stz1stw
89 88 simplbi wDzwHzH
90 89 simprd wDzzH
91 87 90 anim12i vDwwDzvHzH
92 88 simprbi wDz1stz1stw
93 85 simprbi vDw1stw1stv
94 92 93 sylan9ssr vDwwDz1stz1stv
95 1 2 63 71 filnetlem1 vDzvHzH1stz1stv
96 91 94 95 sylanbrc vDwwDzvDz
97 96 ax-gen zvDwwDzvDz
98 97 gen2 vwzvDwwDzvDz
99 cotr DDDvwzvDwwDzvDz
100 98 99 mpbir DDD
101 83 100 jctil FFilXDDDH×HD-1D
102 filtop FFilXXF
103 xpexg FFilXXFF×XV
104 102 103 mpdan FFilXF×XV
105 104 30 ssexd FFilXHV
106 105 105 xpexd FFilXH×HV
107 ssexg DH×HH×HVDV
108 13 106 107 sylancr FFilXDV
109 21 isdir DVDDirRelRelDIHDDDDH×HD-1D
110 108 109 syl FFilXDDirRelRelDIHDDDDH×HD-1D
111 33 101 110 mpbir2and FFilXDDirRel
112 30 111 jca FFilXHF×XDDirRel
113 21 112 pm3.2i H=DFFilXHF×XDDirRel