Metamath Proof Explorer

Theorem fmfnfmlem3

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 19-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b 
|- ( ph -> B e. ( fBas ` Y ) )
fmfnfm.l 
|- ( ph -> L e. ( Fil ` X ) )
fmfnfm.f 
|- ( ph -> F : Y --> X )
fmfnfm.fm 
|- ( ph -> ( ( X FilMap F ) ` B ) C_ L )
Assertion fmfnfmlem3 
|- ( ph -> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b 
 |-  ( ph -> B e. ( fBas ` Y ) )
2 fmfnfm.l 
 |-  ( ph -> L e. ( Fil ` X ) )
3 fmfnfm.f 
 |-  ( ph -> F : Y --> X )
4 fmfnfm.fm 
 |-  ( ph -> ( ( X FilMap F ) ` B ) C_ L )
5 filin 
 |-  ( ( L e. ( Fil ` X ) /\ y e. L /\ z e. L ) -> ( y i^i z ) e. L )
6 5 3expb 
 |-  ( ( L e. ( Fil ` X ) /\ ( y e. L /\ z e. L ) ) -> ( y i^i z ) e. L )
7 2 6 sylan 
 |-  ( ( ph /\ ( y e. L /\ z e. L ) ) -> ( y i^i z ) e. L )
8 ffun 
 |-  ( F : Y --> X -> Fun F )
9 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
10 imain 
 |-  ( Fun `' `' F -> ( `' F " ( y i^i z ) ) = ( ( `' F " y ) i^i ( `' F " z ) ) )
11 10 eqcomd 
 |-  ( Fun `' `' F -> ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " ( y i^i z ) ) )
12 3 8 9 11 4syl 
 |-  ( ph -> ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " ( y i^i z ) ) )
13 12 adantr 
 |-  ( ( ph /\ ( y e. L /\ z e. L ) ) -> ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " ( y i^i z ) ) )
14 imaeq2 
 |-  ( x = ( y i^i z ) -> ( `' F " x ) = ( `' F " ( y i^i z ) ) )
15 14 rspceeqv 
 |-  ( ( ( y i^i z ) e. L /\ ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " ( y i^i z ) ) ) -> E. x e. L ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " x ) )
16 7 13 15 syl2anc 
 |-  ( ( ph /\ ( y e. L /\ z e. L ) ) -> E. x e. L ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " x ) )
17 ineq12 
 |-  ( ( s = ( `' F " y ) /\ t = ( `' F " z ) ) -> ( s i^i t ) = ( ( `' F " y ) i^i ( `' F " z ) ) )
18 17 eqeq1d 
 |-  ( ( s = ( `' F " y ) /\ t = ( `' F " z ) ) -> ( ( s i^i t ) = ( `' F " x ) <-> ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " x ) ) )
19 18 rexbidv 
 |-  ( ( s = ( `' F " y ) /\ t = ( `' F " z ) ) -> ( E. x e. L ( s i^i t ) = ( `' F " x ) <-> E. x e. L ( ( `' F " y ) i^i ( `' F " z ) ) = ( `' F " x ) ) )
20 16 19 syl5ibrcom 
 |-  ( ( ph /\ ( y e. L /\ z e. L ) ) -> ( ( s = ( `' F " y ) /\ t = ( `' F " z ) ) -> E. x e. L ( s i^i t ) = ( `' F " x ) ) )
21 20 rexlimdvva 
 |-  ( ph -> ( E. y e. L E. z e. L ( s = ( `' F " y ) /\ t = ( `' F " z ) ) -> E. x e. L ( s i^i t ) = ( `' F " x ) ) )
22 imaeq2 
 |-  ( x = y -> ( `' F " x ) = ( `' F " y ) )
23 22 eqeq2d 
 |-  ( x = y -> ( s = ( `' F " x ) <-> s = ( `' F " y ) ) )
24 23 cbvrexvw 
 |-  ( E. x e. L s = ( `' F " x ) <-> E. y e. L s = ( `' F " y ) )
25 imaeq2 
 |-  ( x = z -> ( `' F " x ) = ( `' F " z ) )
26 25 eqeq2d 
 |-  ( x = z -> ( t = ( `' F " x ) <-> t = ( `' F " z ) ) )
27 26 cbvrexvw 
 |-  ( E. x e. L t = ( `' F " x ) <-> E. z e. L t = ( `' F " z ) )
28 24 27 anbi12i 
 |-  ( ( E. x e. L s = ( `' F " x ) /\ E. x e. L t = ( `' F " x ) ) <-> ( E. y e. L s = ( `' F " y ) /\ E. z e. L t = ( `' F " z ) ) )
29 eqid 
 |-  ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
30 29 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) ) )
31 30 elv 
 |-  ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) )
32 29 elrnmpt 
 |-  ( t e. _V -> ( t e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L t = ( `' F " x ) ) )
33 32 elv 
 |-  ( t e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L t = ( `' F " x ) )
34 31 33 anbi12i 
 |-  ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ t e. ran ( x e. L |-> ( `' F " x ) ) ) <-> ( E. x e. L s = ( `' F " x ) /\ E. x e. L t = ( `' F " x ) ) )
35 reeanv 
 |-  ( E. y e. L E. z e. L ( s = ( `' F " y ) /\ t = ( `' F " z ) ) <-> ( E. y e. L s = ( `' F " y ) /\ E. z e. L t = ( `' F " z ) ) )
36 28 34 35 3bitr4i 
 |-  ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ t e. ran ( x e. L |-> ( `' F " x ) ) ) <-> E. y e. L E. z e. L ( s = ( `' F " y ) /\ t = ( `' F " z ) ) )
37 vex 
 |-  s e. _V
38 37 inex1 
 |-  ( s i^i t ) e. _V
39 29 elrnmpt 
 |-  ( ( s i^i t ) e. _V -> ( ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( s i^i t ) = ( `' F " x ) ) )
40 38 39 ax-mp 
 |-  ( ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( s i^i t ) = ( `' F " x ) )
41 21 36 40 3imtr4g 
 |-  ( ph -> ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ t e. ran ( x e. L |-> ( `' F " x ) ) ) -> ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) ) )
42 41 ralrimivv 
 |-  ( ph -> A. s e. ran ( x e. L |-> ( `' F " x ) ) A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) )
43 mptexg 
 |-  ( L e. ( Fil ` X ) -> ( x e. L |-> ( `' F " x ) ) e. _V )
44 rnexg 
 |-  ( ( x e. L |-> ( `' F " x ) ) e. _V -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
45 inficl 
 |-  ( ran ( x e. L |-> ( `' F " x ) ) e. _V -> ( A. s e. ran ( x e. L |-> ( `' F " x ) ) A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) ) )
46 2 43 44 45 4syl 
 |-  ( ph -> ( A. s e. ran ( x e. L |-> ( `' F " x ) ) A. t e. ran ( x e. L |-> ( `' F " x ) ) ( s i^i t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) ) )
47 42 46 mpbid 
 |-  ( ph -> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) )