Metamath Proof Explorer

Theorem firest

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

Ref Expression
Assertion firest 
|- ( fi ` ( J |`t A ) ) = ( ( fi ` J ) |`t A )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( J |`t A ) e. _V
2 elfi2 
 |-  ( ( J |`t A ) e. _V -> ( x e. ( fi ` ( J |`t A ) ) <-> E. y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) x = |^| y ) )
3 1 2 ax-mp 
 |-  ( x e. ( fi ` ( J |`t A ) ) <-> E. y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) x = |^| y )
4 eldifi 
 |-  ( y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) -> y e. ( ~P ( J |`t A ) i^i Fin ) )
5 4 adantl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> y e. ( ~P ( J |`t A ) i^i Fin ) )
6 5 elin2d 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> y e. Fin )
7 elfpw 
 |-  ( y e. ( ~P ( J |`t A ) i^i Fin ) <-> ( y C_ ( J |`t A ) /\ y e. Fin ) )
8 7 simplbi 
 |-  ( y e. ( ~P ( J |`t A ) i^i Fin ) -> y C_ ( J |`t A ) )
9 5 8 syl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> y C_ ( J |`t A ) )
10 9 sseld 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( z e. y -> z e. ( J |`t A ) ) )
11 elrest 
 |-  ( ( J e. _V /\ A e. _V ) -> ( z e. ( J |`t A ) <-> E. y e. J z = ( y i^i A ) ) )
12 11 adantr 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( z e. ( J |`t A ) <-> E. y e. J z = ( y i^i A ) ) )
13 10 12 sylibd 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( z e. y -> E. y e. J z = ( y i^i A ) ) )
14 13 ralrimiv 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> A. z e. y E. y e. J z = ( y i^i A ) )
15 ineq1 
 |-  ( y = ( f ` z ) -> ( y i^i A ) = ( ( f ` z ) i^i A ) )
16 15 eqeq2d 
 |-  ( y = ( f ` z ) -> ( z = ( y i^i A ) <-> z = ( ( f ` z ) i^i A ) ) )
17 16 ac6sfi 
 |-  ( ( y e. Fin /\ A. z e. y E. y e. J z = ( y i^i A ) ) -> E. f ( f : y --> J /\ A. z e. y z = ( ( f ` z ) i^i A ) ) )
18 6 14 17 syl2anc 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> E. f ( f : y --> J /\ A. z e. y z = ( ( f ` z ) i^i A ) ) )
19 eldifsni 
 |-  ( y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) -> y =/= (/) )
20 19 ad2antlr 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> y =/= (/) )
21 iinin1 
 |-  ( y =/= (/) -> |^|_ z e. y ( ( f ` z ) i^i A ) = ( |^|_ z e. y ( f ` z ) i^i A ) )
22 20 21 syl 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> |^|_ z e. y ( ( f ` z ) i^i A ) = ( |^|_ z e. y ( f ` z ) i^i A ) )
23 fvex 
 |-  ( fi ` J ) e. _V
24 simpllr 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> A e. _V )
25 ffn 
 |-  ( f : y --> J -> f Fn y )
26 25 adantl 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> f Fn y )
27 fniinfv 
 |-  ( f Fn y -> |^|_ z e. y ( f ` z ) = |^| ran f )
28 26 27 syl 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> |^|_ z e. y ( f ` z ) = |^| ran f )
29 simplll 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> J e. _V )
30 simpr 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> f : y --> J )
31 6 adantr 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> y e. Fin )
32 intrnfi 
 |-  ( ( J e. _V /\ ( f : y --> J /\ y =/= (/) /\ y e. Fin ) ) -> |^| ran f e. ( fi ` J ) )
33 29 30 20 31 32 syl13anc 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> |^| ran f e. ( fi ` J ) )
34 28 33 eqeltrd 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> |^|_ z e. y ( f ` z ) e. ( fi ` J ) )
35 elrestr 
 |-  ( ( ( fi ` J ) e. _V /\ A e. _V /\ |^|_ z e. y ( f ` z ) e. ( fi ` J ) ) -> ( |^|_ z e. y ( f ` z ) i^i A ) e. ( ( fi ` J ) |`t A ) )
36 23 24 34 35 mp3an2i 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> ( |^|_ z e. y ( f ` z ) i^i A ) e. ( ( fi ` J ) |`t A ) )
37 22 36 eqeltrd 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> |^|_ z e. y ( ( f ` z ) i^i A ) e. ( ( fi ` J ) |`t A ) )
38 intiin 
 |-  |^| y = |^|_ z e. y z
39 iineq2 
 |-  ( A. z e. y z = ( ( f ` z ) i^i A ) -> |^|_ z e. y z = |^|_ z e. y ( ( f ` z ) i^i A ) )
40 38 39 eqtrid 
 |-  ( A. z e. y z = ( ( f ` z ) i^i A ) -> |^| y = |^|_ z e. y ( ( f ` z ) i^i A ) )
41 40 eleq1d 
 |-  ( A. z e. y z = ( ( f ` z ) i^i A ) -> ( |^| y e. ( ( fi ` J ) |`t A ) <-> |^|_ z e. y ( ( f ` z ) i^i A ) e. ( ( fi ` J ) |`t A ) ) )
42 37 41 syl5ibrcom 
 |-  ( ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) /\ f : y --> J ) -> ( A. z e. y z = ( ( f ` z ) i^i A ) -> |^| y e. ( ( fi ` J ) |`t A ) ) )
43 42 expimpd 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( ( f : y --> J /\ A. z e. y z = ( ( f ` z ) i^i A ) ) -> |^| y e. ( ( fi ` J ) |`t A ) ) )
44 43 exlimdv 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( E. f ( f : y --> J /\ A. z e. y z = ( ( f ` z ) i^i A ) ) -> |^| y e. ( ( fi ` J ) |`t A ) ) )
45 18 44 mpd 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> |^| y e. ( ( fi ` J ) |`t A ) )
46 eleq1 
 |-  ( x = |^| y -> ( x e. ( ( fi ` J ) |`t A ) <-> |^| y e. ( ( fi ` J ) |`t A ) ) )
47 45 46 syl5ibrcom 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) ) -> ( x = |^| y -> x e. ( ( fi ` J ) |`t A ) ) )
48 47 rexlimdva 
 |-  ( ( J e. _V /\ A e. _V ) -> ( E. y e. ( ( ~P ( J |`t A ) i^i Fin ) \ { (/) } ) x = |^| y -> x e. ( ( fi ` J ) |`t A ) ) )
49 3 48 syl5bi 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( fi ` ( J |`t A ) ) -> x e. ( ( fi ` J ) |`t A ) ) )
50 simpr 
 |-  ( ( J e. _V /\ A e. _V ) -> A e. _V )
51 elrest 
 |-  ( ( ( fi ` J ) e. _V /\ A e. _V ) -> ( x e. ( ( fi ` J ) |`t A ) <-> E. z e. ( fi ` J ) x = ( z i^i A ) ) )
52 23 50 51 sylancr 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( ( fi ` J ) |`t A ) <-> E. z e. ( fi ` J ) x = ( z i^i A ) ) )
53 elfi2 
 |-  ( J e. _V -> ( z e. ( fi ` J ) <-> E. y e. ( ( ~P J i^i Fin ) \ { (/) } ) z = |^| y ) )
54 53 adantr 
 |-  ( ( J e. _V /\ A e. _V ) -> ( z e. ( fi ` J ) <-> E. y e. ( ( ~P J i^i Fin ) \ { (/) } ) z = |^| y ) )
55 eldifsni 
 |-  ( y e. ( ( ~P J i^i Fin ) \ { (/) } ) -> y =/= (/) )
56 55 adantl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> y =/= (/) )
57 iinin1 
 |-  ( y =/= (/) -> |^|_ z e. y ( z i^i A ) = ( |^|_ z e. y z i^i A ) )
58 56 57 syl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> |^|_ z e. y ( z i^i A ) = ( |^|_ z e. y z i^i A ) )
59 38 ineq1i 
 |-  ( |^| y i^i A ) = ( |^|_ z e. y z i^i A )
60 58 59 eqtr4di 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> |^|_ z e. y ( z i^i A ) = ( |^| y i^i A ) )
61 ovexd 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> ( J |`t A ) e. _V )
62 eldifi 
 |-  ( y e. ( ( ~P J i^i Fin ) \ { (/) } ) -> y e. ( ~P J i^i Fin ) )
63 62 adantl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> y e. ( ~P J i^i Fin ) )
64 elfpw 
 |-  ( y e. ( ~P J i^i Fin ) <-> ( y C_ J /\ y e. Fin ) )
65 64 simplbi 
 |-  ( y e. ( ~P J i^i Fin ) -> y C_ J )
66 63 65 syl 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> y C_ J )
67 elrestr 
 |-  ( ( J e. _V /\ A e. _V /\ z e. J ) -> ( z i^i A ) e. ( J |`t A ) )
68 67 3expa 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ z e. J ) -> ( z i^i A ) e. ( J |`t A ) )
69 68 ralrimiva 
 |-  ( ( J e. _V /\ A e. _V ) -> A. z e. J ( z i^i A ) e. ( J |`t A ) )
70 69 adantr 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> A. z e. J ( z i^i A ) e. ( J |`t A ) )
71 ssralv 
 |-  ( y C_ J -> ( A. z e. J ( z i^i A ) e. ( J |`t A ) -> A. z e. y ( z i^i A ) e. ( J |`t A ) ) )
72 66 70 71 sylc 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> A. z e. y ( z i^i A ) e. ( J |`t A ) )
73 63 elin2d 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> y e. Fin )
74 iinfi 
 |-  ( ( ( J |`t A ) e. _V /\ ( A. z e. y ( z i^i A ) e. ( J |`t A ) /\ y =/= (/) /\ y e. Fin ) ) -> |^|_ z e. y ( z i^i A ) e. ( fi ` ( J |`t A ) ) )
75 61 72 56 73 74 syl13anc 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> |^|_ z e. y ( z i^i A ) e. ( fi ` ( J |`t A ) ) )
76 60 75 eqeltrrd 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> ( |^| y i^i A ) e. ( fi ` ( J |`t A ) ) )
77 eleq1 
 |-  ( x = ( |^| y i^i A ) -> ( x e. ( fi ` ( J |`t A ) ) <-> ( |^| y i^i A ) e. ( fi ` ( J |`t A ) ) ) )
78 76 77 syl5ibrcom 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> ( x = ( |^| y i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) )
79 ineq1 
 |-  ( z = |^| y -> ( z i^i A ) = ( |^| y i^i A ) )
80 79 eqeq2d 
 |-  ( z = |^| y -> ( x = ( z i^i A ) <-> x = ( |^| y i^i A ) ) )
81 80 imbi1d 
 |-  ( z = |^| y -> ( ( x = ( z i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) <-> ( x = ( |^| y i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) ) )
82 78 81 syl5ibrcom 
 |-  ( ( ( J e. _V /\ A e. _V ) /\ y e. ( ( ~P J i^i Fin ) \ { (/) } ) ) -> ( z = |^| y -> ( x = ( z i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) ) )
83 82 rexlimdva 
 |-  ( ( J e. _V /\ A e. _V ) -> ( E. y e. ( ( ~P J i^i Fin ) \ { (/) } ) z = |^| y -> ( x = ( z i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) ) )
84 54 83 sylbid 
 |-  ( ( J e. _V /\ A e. _V ) -> ( z e. ( fi ` J ) -> ( x = ( z i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) ) )
85 84 rexlimdv 
 |-  ( ( J e. _V /\ A e. _V ) -> ( E. z e. ( fi ` J ) x = ( z i^i A ) -> x e. ( fi ` ( J |`t A ) ) ) )
86 52 85 sylbid 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( ( fi ` J ) |`t A ) -> x e. ( fi ` ( J |`t A ) ) ) )
87 49 86 impbid 
 |-  ( ( J e. _V /\ A e. _V ) -> ( x e. ( fi ` ( J |`t A ) ) <-> x e. ( ( fi ` J ) |`t A ) ) )
88 87 eqrdv 
 |-  ( ( J e. _V /\ A e. _V ) -> ( fi ` ( J |`t A ) ) = ( ( fi ` J ) |`t A ) )
89 fi0 
 |-  ( fi ` (/) ) = (/)
90 relxp 
 |-  Rel ( _V X. _V )
91 restfn 
 |-  |`t Fn ( _V X. _V )
92 91 fndmi 
 |-  dom |`t = ( _V X. _V )
93 92 releqi 
 |-  ( Rel dom |`t <-> Rel ( _V X. _V ) )
94 90 93 mpbir 
 |-  Rel dom |`t
95 94 ovprc 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
96 95 fveq2d 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( fi ` ( J |`t A ) ) = ( fi ` (/) ) )
97 ianor 
 |-  ( -. ( J e. _V /\ A e. _V ) <-> ( -. J e. _V \/ -. A e. _V ) )
98 fvprc 
 |-  ( -. J e. _V -> ( fi ` J ) = (/) )
99 98 oveq1d 
 |-  ( -. J e. _V -> ( ( fi ` J ) |`t A ) = ( (/) |`t A ) )
100 0rest 
 |-  ( (/) |`t A ) = (/)
101 99 100 eqtrdi 
 |-  ( -. J e. _V -> ( ( fi ` J ) |`t A ) = (/) )
102 94 ovprc2 
 |-  ( -. A e. _V -> ( ( fi ` J ) |`t A ) = (/) )
103 101 102 jaoi 
 |-  ( ( -. J e. _V \/ -. A e. _V ) -> ( ( fi ` J ) |`t A ) = (/) )
104 97 103 sylbi 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( ( fi ` J ) |`t A ) = (/) )
105 89 96 104 3eqtr4a 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( fi ` ( J |`t A ) ) = ( ( fi ` J ) |`t A ) )
106 88 105 pm2.61i 
 |-  ( fi ` ( J |`t A ) ) = ( ( fi ` J ) |`t A )