Metamath Proof Explorer


Theorem firest

Description: The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion firest fiJ𝑡A=fiJ𝑡A

Proof

Step Hyp Ref Expression
1 ovex J𝑡AV
2 elfi2 J𝑡AVxfiJ𝑡Ay𝒫J𝑡AFinx=y
3 1 2 ax-mp xfiJ𝑡Ay𝒫J𝑡AFinx=y
4 eldifi y𝒫J𝑡AFiny𝒫J𝑡AFin
5 4 adantl JVAVy𝒫J𝑡AFiny𝒫J𝑡AFin
6 5 elin2d JVAVy𝒫J𝑡AFinyFin
7 elfpw y𝒫J𝑡AFinyJ𝑡AyFin
8 7 simplbi y𝒫J𝑡AFinyJ𝑡A
9 5 8 syl JVAVy𝒫J𝑡AFinyJ𝑡A
10 9 sseld JVAVy𝒫J𝑡AFinzyzJ𝑡A
11 elrest JVAVzJ𝑡AyJz=yA
12 11 adantr JVAVy𝒫J𝑡AFinzJ𝑡AyJz=yA
13 10 12 sylibd JVAVy𝒫J𝑡AFinzyyJz=yA
14 13 ralrimiv JVAVy𝒫J𝑡AFinzyyJz=yA
15 ineq1 y=fzyA=fzA
16 15 eqeq2d y=fzz=yAz=fzA
17 16 ac6sfi yFinzyyJz=yAff:yJzyz=fzA
18 6 14 17 syl2anc JVAVy𝒫J𝑡AFinff:yJzyz=fzA
19 eldifsni y𝒫J𝑡AFiny
20 19 ad2antlr JVAVy𝒫J𝑡AFinf:yJy
21 iinin1 yzyfzA=zyfzA
22 20 21 syl JVAVy𝒫J𝑡AFinf:yJzyfzA=zyfzA
23 fvex fiJV
24 simpllr JVAVy𝒫J𝑡AFinf:yJAV
25 ffn f:yJfFny
26 25 adantl JVAVy𝒫J𝑡AFinf:yJfFny
27 fniinfv fFnyzyfz=ranf
28 26 27 syl JVAVy𝒫J𝑡AFinf:yJzyfz=ranf
29 simplll JVAVy𝒫J𝑡AFinf:yJJV
30 simpr JVAVy𝒫J𝑡AFinf:yJf:yJ
31 6 adantr JVAVy𝒫J𝑡AFinf:yJyFin
32 intrnfi JVf:yJyyFinranffiJ
33 29 30 20 31 32 syl13anc JVAVy𝒫J𝑡AFinf:yJranffiJ
34 28 33 eqeltrd JVAVy𝒫J𝑡AFinf:yJzyfzfiJ
35 elrestr fiJVAVzyfzfiJzyfzAfiJ𝑡A
36 23 24 34 35 mp3an2i JVAVy𝒫J𝑡AFinf:yJzyfzAfiJ𝑡A
37 22 36 eqeltrd JVAVy𝒫J𝑡AFinf:yJzyfzAfiJ𝑡A
38 intiin y=zyz
39 iineq2 zyz=fzAzyz=zyfzA
40 38 39 eqtrid zyz=fzAy=zyfzA
41 40 eleq1d zyz=fzAyfiJ𝑡AzyfzAfiJ𝑡A
42 37 41 syl5ibrcom JVAVy𝒫J𝑡AFinf:yJzyz=fzAyfiJ𝑡A
43 42 expimpd JVAVy𝒫J𝑡AFinf:yJzyz=fzAyfiJ𝑡A
44 43 exlimdv JVAVy𝒫J𝑡AFinff:yJzyz=fzAyfiJ𝑡A
45 18 44 mpd JVAVy𝒫J𝑡AFinyfiJ𝑡A
46 eleq1 x=yxfiJ𝑡AyfiJ𝑡A
47 45 46 syl5ibrcom JVAVy𝒫J𝑡AFinx=yxfiJ𝑡A
48 47 rexlimdva JVAVy𝒫J𝑡AFinx=yxfiJ𝑡A
49 3 48 syl5bi JVAVxfiJ𝑡AxfiJ𝑡A
50 simpr JVAVAV
51 elrest fiJVAVxfiJ𝑡AzfiJx=zA
52 23 50 51 sylancr JVAVxfiJ𝑡AzfiJx=zA
53 elfi2 JVzfiJy𝒫JFinz=y
54 53 adantr JVAVzfiJy𝒫JFinz=y
55 eldifsni y𝒫JFiny
56 55 adantl JVAVy𝒫JFiny
57 iinin1 yzyzA=zyzA
58 56 57 syl JVAVy𝒫JFinzyzA=zyzA
59 38 ineq1i yA=zyzA
60 58 59 eqtr4di JVAVy𝒫JFinzyzA=yA
61 ovexd JVAVy𝒫JFinJ𝑡AV
62 eldifi y𝒫JFiny𝒫JFin
63 62 adantl JVAVy𝒫JFiny𝒫JFin
64 elfpw y𝒫JFinyJyFin
65 64 simplbi y𝒫JFinyJ
66 63 65 syl JVAVy𝒫JFinyJ
67 elrestr JVAVzJzAJ𝑡A
68 67 3expa JVAVzJzAJ𝑡A
69 68 ralrimiva JVAVzJzAJ𝑡A
70 69 adantr JVAVy𝒫JFinzJzAJ𝑡A
71 ssralv yJzJzAJ𝑡AzyzAJ𝑡A
72 66 70 71 sylc JVAVy𝒫JFinzyzAJ𝑡A
73 63 elin2d JVAVy𝒫JFinyFin
74 iinfi J𝑡AVzyzAJ𝑡AyyFinzyzAfiJ𝑡A
75 61 72 56 73 74 syl13anc JVAVy𝒫JFinzyzAfiJ𝑡A
76 60 75 eqeltrrd JVAVy𝒫JFinyAfiJ𝑡A
77 eleq1 x=yAxfiJ𝑡AyAfiJ𝑡A
78 76 77 syl5ibrcom JVAVy𝒫JFinx=yAxfiJ𝑡A
79 ineq1 z=yzA=yA
80 79 eqeq2d z=yx=zAx=yA
81 80 imbi1d z=yx=zAxfiJ𝑡Ax=yAxfiJ𝑡A
82 78 81 syl5ibrcom JVAVy𝒫JFinz=yx=zAxfiJ𝑡A
83 82 rexlimdva JVAVy𝒫JFinz=yx=zAxfiJ𝑡A
84 54 83 sylbid JVAVzfiJx=zAxfiJ𝑡A
85 84 rexlimdv JVAVzfiJx=zAxfiJ𝑡A
86 52 85 sylbid JVAVxfiJ𝑡AxfiJ𝑡A
87 49 86 impbid JVAVxfiJ𝑡AxfiJ𝑡A
88 87 eqrdv JVAVfiJ𝑡A=fiJ𝑡A
89 fi0 fi=
90 relxp RelV×V
91 restfn 𝑡FnV×V
92 91 fndmi dom𝑡=V×V
93 92 releqi Reldom𝑡RelV×V
94 90 93 mpbir Reldom𝑡
95 94 ovprc ¬JVAVJ𝑡A=
96 95 fveq2d ¬JVAVfiJ𝑡A=fi
97 ianor ¬JVAV¬JV¬AV
98 fvprc ¬JVfiJ=
99 98 oveq1d ¬JVfiJ𝑡A=𝑡A
100 0rest 𝑡A=
101 99 100 eqtrdi ¬JVfiJ𝑡A=
102 94 ovprc2 ¬AVfiJ𝑡A=
103 101 102 jaoi ¬JV¬AVfiJ𝑡A=
104 97 103 sylbi ¬JVAVfiJ𝑡A=
105 89 96 104 3eqtr4a ¬JVAVfiJ𝑡A=fiJ𝑡A
106 88 105 pm2.61i fiJ𝑡A=fiJ𝑡A