Metamath Proof Explorer

Theorem fmfnfmlem4

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 fmfnfmlem4 
|- ( ph -> ( t e. L <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )

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 filelss 
 |-  ( ( L e. ( Fil ` X ) /\ t e. L ) -> t C_ X )
6 5 ex 
 |-  ( L e. ( Fil ` X ) -> ( t e. L -> t C_ X ) )
7 2 6 syl 
 |-  ( ph -> ( t e. L -> t C_ X ) )
8 mptexg 
 |-  ( L e. ( Fil ` X ) -> ( x e. L |-> ( `' F " x ) ) e. _V )
9 rnexg 
 |-  ( ( x e. L |-> ( `' F " x ) ) e. _V -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
10 8 9 syl 
 |-  ( L e. ( Fil ` X ) -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
11 2 10 syl 
 |-  ( ph -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
12 unexg 
 |-  ( ( B e. ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. _V ) -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
13 1 11 12 syl2anc 
 |-  ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
14 ssfii 
 |-  ( ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
15 14 unssbd 
 |-  ( ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V -> ran ( x e. L |-> ( `' F " x ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
16 13 15 syl 
 |-  ( ph -> ran ( x e. L |-> ( `' F " x ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
17 16 adantr 
 |-  ( ( ph /\ t e. L ) -> ran ( x e. L |-> ( `' F " x ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
18 eqid 
 |-  ( `' F " t ) = ( `' F " t )
19 imaeq2 
 |-  ( x = t -> ( `' F " x ) = ( `' F " t ) )
20 19 rspceeqv 
 |-  ( ( t e. L /\ ( `' F " t ) = ( `' F " t ) ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
21 18 20 mpan2 
 |-  ( t e. L -> E. x e. L ( `' F " t ) = ( `' F " x ) )
22 21 adantl 
 |-  ( ( ph /\ t e. L ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
23 elfvdm 
 |-  ( B e. ( fBas ` Y ) -> Y e. dom fBas )
24 1 23 syl 
 |-  ( ph -> Y e. dom fBas )
25 cnvimass 
 |-  ( `' F " t ) C_ dom F
26 25 3 fssdm 
 |-  ( ph -> ( `' F " t ) C_ Y )
27 24 26 ssexd 
 |-  ( ph -> ( `' F " t ) e. _V )
28 27 adantr 
 |-  ( ( ph /\ t e. L ) -> ( `' F " t ) e. _V )
29 eqid 
 |-  ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
30 29 elrnmpt 
 |-  ( ( `' F " t ) e. _V -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
31 28 30 syl 
 |-  ( ( ph /\ t e. L ) -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
32 22 31 mpbird 
 |-  ( ( ph /\ t e. L ) -> ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) )
33 17 32 sseldd 
 |-  ( ( ph /\ t e. L ) -> ( `' F " t ) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
34 ffun 
 |-  ( F : Y --> X -> Fun F )
35 ssid 
 |-  ( `' F " t ) C_ ( `' F " t )
36 funimass2 
 |-  ( ( Fun F /\ ( `' F " t ) C_ ( `' F " t ) ) -> ( F " ( `' F " t ) ) C_ t )
37 34 35 36 sylancl 
 |-  ( F : Y --> X -> ( F " ( `' F " t ) ) C_ t )
38 3 37 syl 
 |-  ( ph -> ( F " ( `' F " t ) ) C_ t )
39 38 adantr 
 |-  ( ( ph /\ t e. L ) -> ( F " ( `' F " t ) ) C_ t )
40 imaeq2 
 |-  ( s = ( `' F " t ) -> ( F " s ) = ( F " ( `' F " t ) ) )
41 40 sseq1d 
 |-  ( s = ( `' F " t ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " t ) ) C_ t ) )
42 41 rspcev 
 |-  ( ( ( `' F " t ) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) /\ ( F " ( `' F " t ) ) C_ t ) -> E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t )
43 33 39 42 syl2anc 
 |-  ( ( ph /\ t e. L ) -> E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t )
44 43 ex 
 |-  ( ph -> ( t e. L -> E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) )
45 7 44 jcad 
 |-  ( ph -> ( t e. L -> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
46 elfiun 
 |-  ( ( B e. ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. _V ) -> ( s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) <-> ( s e. ( fi ` B ) \/ s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) \/ E. z e. ( fi ` B ) E. w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) s = ( z i^i w ) ) ) )
47 1 11 46 syl2anc 
 |-  ( ph -> ( s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) <-> ( s e. ( fi ` B ) \/ s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) \/ E. z e. ( fi ` B ) E. w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) s = ( z i^i w ) ) ) )
48 1 2 3 4 fmfnfmlem1 
 |-  ( ph -> ( s e. ( fi ` B ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
49 1 2 3 4 fmfnfmlem3 
 |-  ( ph -> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) )
50 49 eleq2d 
 |-  ( ph -> ( s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> s e. ran ( x e. L |-> ( `' F " x ) ) ) )
51 29 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) ) )
52 51 elv 
 |-  ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) )
53 1 2 3 4 fmfnfmlem2 
 |-  ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
54 52 53 syl5bi 
 |-  ( ph -> ( s e. ran ( x e. L |-> ( `' F " x ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
55 50 54 sylbid 
 |-  ( ph -> ( s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
56 49 eleq2d 
 |-  ( ph -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> w e. ran ( x e. L |-> ( `' F " x ) ) ) )
57 29 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L w = ( `' F " x ) ) )
58 57 elv 
 |-  ( w e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L w = ( `' F " x ) )
59 56 58 bitrdi 
 |-  ( ph -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> E. x e. L w = ( `' F " x ) ) )
60 59 adantr 
 |-  ( ( ph /\ z e. ( fi ` B ) ) -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> E. x e. L w = ( `' F " x ) ) )
61 fbssfi 
 |-  ( ( B e. ( fBas ` Y ) /\ z e. ( fi ` B ) ) -> E. s e. B s C_ z )
62 1 61 sylan 
 |-  ( ( ph /\ z e. ( fi ` B ) ) -> E. s e. B s C_ z )
63 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> L e. ( Fil ` X ) )
64 2 adantr 
 |-  ( ( ph /\ ( s e. B /\ s C_ z ) ) -> L e. ( Fil ` X ) )
65 4 adantr 
 |-  ( ( ph /\ s e. B ) -> ( ( X FilMap F ) ` B ) C_ L )
66 filtop 
 |-  ( L e. ( Fil ` X ) -> X e. L )
67 2 66 syl 
 |-  ( ph -> X e. L )
68 67 1 3 3jca 
 |-  ( ph -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
69 68 adantr 
 |-  ( ( ph /\ s e. B ) -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
70 ssfg 
 |-  ( B e. ( fBas ` Y ) -> B C_ ( Y filGen B ) )
71 1 70 syl 
 |-  ( ph -> B C_ ( Y filGen B ) )
72 71 sselda 
 |-  ( ( ph /\ s e. B ) -> s e. ( Y filGen B ) )
73 eqid 
 |-  ( Y filGen B ) = ( Y filGen B )
74 73 imaelfm 
 |-  ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ s e. ( Y filGen B ) ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
75 69 72 74 syl2anc 
 |-  ( ( ph /\ s e. B ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
76 65 75 sseldd 
 |-  ( ( ph /\ s e. B ) -> ( F " s ) e. L )
77 76 adantrr 
 |-  ( ( ph /\ ( s e. B /\ s C_ z ) ) -> ( F " s ) e. L )
78 64 77 jca 
 |-  ( ( ph /\ ( s e. B /\ s C_ z ) ) -> ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) )
79 filin 
 |-  ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
80 79 3expa 
 |-  ( ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
81 78 80 sylan 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
82 81 adantr 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> ( ( F " s ) i^i x ) e. L )
83 simprr 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> t C_ X )
84 elin 
 |-  ( w e. ( ( F " s ) i^i x ) <-> ( w e. ( F " s ) /\ w e. x ) )
85 3 34 syl 
 |-  ( ph -> Fun F )
86 fvelima 
 |-  ( ( Fun F /\ w e. ( F " s ) ) -> E. y e. s ( F ` y ) = w )
87 86 ex 
 |-  ( Fun F -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
88 85 87 syl 
 |-  ( ph -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
89 88 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
90 85 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> Fun F )
91 simplrr 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> s C_ z )
92 simprl 
 |-  ( ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) -> y e. s )
93 ssel2 
 |-  ( ( s C_ z /\ y e. s ) -> y e. z )
94 91 92 93 syl2an 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> y e. z )
95 85 ad2antrr 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> Fun F )
96 fbelss 
 |-  ( ( B e. ( fBas ` Y ) /\ s e. B ) -> s C_ Y )
97 1 96 sylan 
 |-  ( ( ph /\ s e. B ) -> s C_ Y )
98 3 fdmd 
 |-  ( ph -> dom F = Y )
99 98 adantr 
 |-  ( ( ph /\ s e. B ) -> dom F = Y )
100 97 99 sseqtrrd 
 |-  ( ( ph /\ s e. B ) -> s C_ dom F )
101 100 adantrr 
 |-  ( ( ph /\ ( s e. B /\ s C_ z ) ) -> s C_ dom F )
102 101 sselda 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> y e. dom F )
103 fvimacnv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
104 95 102 103 syl2anc 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
105 104 biimpd 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> ( ( F ` y ) e. x -> y e. ( `' F " x ) ) )
106 105 impr 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ ( y e. s /\ ( F ` y ) e. x ) ) -> y e. ( `' F " x ) )
107 106 ad2ant2rl 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> y e. ( `' F " x ) )
108 94 107 elind 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> y e. ( z i^i ( `' F " x ) ) )
109 inss2 
 |-  ( z i^i ( `' F " x ) ) C_ ( `' F " x )
110 cnvimass 
 |-  ( `' F " x ) C_ dom F
111 109 110 sstri 
 |-  ( z i^i ( `' F " x ) ) C_ dom F
112 funfvima2 
 |-  ( ( Fun F /\ ( z i^i ( `' F " x ) ) C_ dom F ) -> ( y e. ( z i^i ( `' F " x ) ) -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) ) )
113 111 112 mpan2 
 |-  ( Fun F -> ( y e. ( z i^i ( `' F " x ) ) -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) ) )
114 90 108 113 sylc 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) )
115 114 anassrs 
 |-  ( ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) /\ ( y e. s /\ ( F ` y ) e. x ) ) -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) )
116 115 expr 
 |-  ( ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) /\ y e. s ) -> ( ( F ` y ) e. x -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) ) )
117 eleq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) e. x <-> w e. x ) )
118 eleq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) <-> w e. ( F " ( z i^i ( `' F " x ) ) ) ) )
119 117 118 imbi12d 
 |-  ( ( F ` y ) = w -> ( ( ( F ` y ) e. x -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) ) <-> ( w e. x -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) ) )
120 116 119 syl5ibcom 
 |-  ( ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) /\ y e. s ) -> ( ( F ` y ) = w -> ( w e. x -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) ) )
121 120 rexlimdva 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( E. y e. s ( F ` y ) = w -> ( w e. x -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) ) )
122 89 121 syld 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( w e. ( F " s ) -> ( w e. x -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) ) )
123 122 impd 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( ( w e. ( F " s ) /\ w e. x ) -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) )
124 84 123 syl5bi 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( w e. ( ( F " s ) i^i x ) -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) )
125 124 adantrl 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> ( w e. ( ( F " s ) i^i x ) -> w e. ( F " ( z i^i ( `' F " x ) ) ) ) )
126 125 ssrdv 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> ( ( F " s ) i^i x ) C_ ( F " ( z i^i ( `' F " x ) ) ) )
127 simprl 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> ( F " ( z i^i ( `' F " x ) ) ) C_ t )
128 126 127 sstrd 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> ( ( F " s ) i^i x ) C_ t )
129 filss 
 |-  ( ( L e. ( Fil ` X ) /\ ( ( ( F " s ) i^i x ) e. L /\ t C_ X /\ ( ( F " s ) i^i x ) C_ t ) ) -> t e. L )
130 63 82 83 128 129 syl13anc 
 |-  ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> t e. L )
131 130 exp32 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> ( ( F " ( z i^i ( `' F " x ) ) ) C_ t -> ( t C_ X -> t e. L ) ) )
132 ineq2 
 |-  ( w = ( `' F " x ) -> ( z i^i w ) = ( z i^i ( `' F " x ) ) )
133 132 imaeq2d 
 |-  ( w = ( `' F " x ) -> ( F " ( z i^i w ) ) = ( F " ( z i^i ( `' F " x ) ) ) )
134 133 sseq1d 
 |-  ( w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t <-> ( F " ( z i^i ( `' F " x ) ) ) C_ t ) )
135 134 imbi1d 
 |-  ( w = ( `' F " x ) -> ( ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) <-> ( ( F " ( z i^i ( `' F " x ) ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
136 131 135 syl5ibrcom 
 |-  ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> ( w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
137 136 rexlimdva 
 |-  ( ( ph /\ ( s e. B /\ s C_ z ) ) -> ( E. x e. L w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
138 137 rexlimdvaa 
 |-  ( ph -> ( E. s e. B s C_ z -> ( E. x e. L w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) ) )
139 138 imp 
 |-  ( ( ph /\ E. s e. B s C_ z ) -> ( E. x e. L w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
140 62 139 syldan 
 |-  ( ( ph /\ z e. ( fi ` B ) ) -> ( E. x e. L w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
141 60 140 sylbid 
 |-  ( ( ph /\ z e. ( fi ` B ) ) -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
142 141 impr 
 |-  ( ( ph /\ ( z e. ( fi ` B ) /\ w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) )
143 imaeq2 
 |-  ( s = ( z i^i w ) -> ( F " s ) = ( F " ( z i^i w ) ) )
144 143 sseq1d 
 |-  ( s = ( z i^i w ) -> ( ( F " s ) C_ t <-> ( F " ( z i^i w ) ) C_ t ) )
145 144 imbi1d 
 |-  ( s = ( z i^i w ) -> ( ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) <-> ( ( F " ( z i^i w ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
146 142 145 syl5ibrcom 
 |-  ( ( ph /\ ( z e. ( fi ` B ) /\ w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) ) ) -> ( s = ( z i^i w ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
147 146 rexlimdvva 
 |-  ( ph -> ( E. z e. ( fi ` B ) E. w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) s = ( z i^i w ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
148 48 55 147 3jaod 
 |-  ( ph -> ( ( s e. ( fi ` B ) \/ s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) \/ E. z e. ( fi ` B ) E. w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) s = ( z i^i w ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
149 47 148 sylbid 
 |-  ( ph -> ( s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
150 149 rexlimdv 
 |-  ( ph -> ( E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) )
151 150 impcomd 
 |-  ( ph -> ( ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) -> t e. L ) )
152 45 151 impbid 
 |-  ( ph -> ( t e. L <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )