Theorem fmfnfmlem4 21050

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

Hypotheses

Ref	Expression
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

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

Distinct variable groups:   t, s, x, B   F, s, t, x   L, s, t, x   ph, s, t, x   X, s, t, x   Y, s, t, x

Proof of Theorem fmfnfmlem4

Dummy variables w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmfnfm.l	. . . 4 |- ( ph -> L e. ( Fil ` X ) )
2		filelss 20945	. . . . 5 |- ( ( L e. ( Fil ` X ) /\ t e. L ) -> t C_ X )
3	2	ex 441	. . . 4 |- ( L e. ( Fil ` X ) -> ( t e. L -> t C_ X ) )
4	1, 3	syl 17	. . 3 |- ( ph -> ( t e. L -> t C_ X ) )
5		fmfnfm.b	. . . . . . . . 9 |- ( ph -> B e. ( fBas ` Y ) )
6		mptexg 6151	. . . . . . . . . . 11 |- ( L e. ( Fil ` X ) -> ( x e. L |-> ( `' F " x ) ) e. _V )
7		rnexg 6744	. . . . . . . . . . 11 |- ( ( x e. L |-> ( `' F " x ) ) e. _V -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
8	6, 7	syl 17	. . . . . . . . . 10 |- ( L e. ( Fil ` X ) -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
9	1, 8	syl 17	. . . . . . . . 9 |- ( ph -> ran ( x e. L |-> ( `' F " x ) ) e. _V )
10		unexg 6611	. . . . . . . . 9 |- ( ( B e. ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. _V ) -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
11	5, 9, 10	syl2anc 673	. . . . . . . 8 |- ( ph -> ( B u. ran ( x e. L |-> ( `' F " x ) ) ) e. _V )
12		ssfii 7951	. . . . . . . . 9 |- ( ( 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 ) ) ) ) )
13	12	unssbd 3603	. . . . . . . 8 |- ( ( 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 ) ) ) ) )
14	11, 13	syl 17	. . . . . . 7 |- ( ph -> ran ( x e. L |-> ( `' F " x ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
15	14	adantr 472	. . . . . 6 |- ( ( ph /\ t e. L ) -> ran ( x e. L |-> ( `' F " x ) ) C_ ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
16		eqid 2471	. . . . . . . . 9 |- ( `' F " t ) = ( `' F " t )
17		imaeq2 5170	. . . . . . . . . . 11 |- ( x = t -> ( `' F " x ) = ( `' F " t ) )
18	17	eqeq2d 2481	. . . . . . . . . 10 |- ( x = t -> ( ( `' F " t ) = ( `' F " x ) <-> ( `' F " t ) = ( `' F " t ) ) )
19	18	rspcev 3136	. . . . . . . . 9 |- ( ( t e. L /\ ( `' F " t ) = ( `' F " t ) ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
20	16, 19	mpan2 685	. . . . . . . 8 |- ( t e. L -> E. x e. L ( `' F " t ) = ( `' F " x ) )
21	20	adantl 473	. . . . . . 7 |- ( ( ph /\ t e. L ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
22		elfvdm 5905	. . . . . . . . . . 11 |- ( B e. ( fBas ` Y ) -> Y e. dom fBas )
23	5, 22	syl 17	. . . . . . . . . 10 |- ( ph -> Y e. dom fBas )
24		cnvimass 5194	. . . . . . . . . . 11 |- ( `' F " t ) C_ dom F
25		fmfnfm.f	. . . . . . . . . . . 12 |- ( ph -> F : Y --> X )
26		fdm 5745	. . . . . . . . . . . 12 |- ( F : Y --> X -> dom F = Y )
27	25, 26	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = Y )
28	24, 27	syl5sseq 3466	. . . . . . . . . 10 |- ( ph -> ( `' F " t ) C_ Y )
29	23, 28	ssexd 4543	. . . . . . . . 9 |- ( ph -> ( `' F " t ) e. _V )
30	29	adantr 472	. . . . . . . 8 |- ( ( ph /\ t e. L ) -> ( `' F " t ) e. _V )
31		eqid 2471	. . . . . . . . 9 |- ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
32	31	elrnmpt 5087	. . . . . . . 8 |- ( ( `' F " t ) e. _V -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
33	30, 32	syl 17	. . . . . . 7 |- ( ( ph /\ t e. L ) -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
34	21, 33	mpbird 240	. . . . . 6 |- ( ( ph /\ t e. L ) -> ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) )
35	15, 34	sseldd 3419	. . . . 5 |- ( ( ph /\ t e. L ) -> ( `' F " t ) e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) )
36		ffun 5742	. . . . . . . 8 |- ( F : Y --> X -> Fun F )
37		ssid 3437	. . . . . . . 8 |- ( `' F " t ) C_ ( `' F " t )
38		funimass2 5667	. . . . . . . 8 |- ( ( Fun F /\ ( `' F " t ) C_ ( `' F " t ) ) -> ( F " ( `' F " t ) ) C_ t )
39	36, 37, 38	sylancl 675	. . . . . . 7 |- ( F : Y --> X -> ( F " ( `' F " t ) ) C_ t )
40	25, 39	syl 17	. . . . . 6 |- ( ph -> ( F " ( `' F " t ) ) C_ t )
41	40	adantr 472	. . . . 5 |- ( ( ph /\ t e. L ) -> ( F " ( `' F " t ) ) C_ t )
42		imaeq2 5170	. . . . . . 7 |- ( s = ( `' F " t ) -> ( F " s ) = ( F " ( `' F " t ) ) )
43	42	sseq1d 3445	. . . . . 6 |- ( s = ( `' F " t ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " t ) ) C_ t ) )
44	43	rspcev 3136	. . . . 5 |- ( ( ( `' 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 )
45	35, 41, 44	syl2anc 673	. . . 4 |- ( ( ph /\ t e. L ) -> E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t )
46	45	ex 441	. . 3 |- ( ph -> ( t e. L -> E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) )
47	4, 46	jcad 542	. 2 |- ( ph -> ( t e. L -> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
48		elfiun 7962	. . . . . . 7 |- ( ( 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 ) ) ) )
49	5, 9, 48	syl2anc 673	. . . . . 6 |- ( 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 ) ) ) )
50		fmfnfm.fm	. . . . . . . 8 |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )
51	5, 1, 25, 50	fmfnfmlem1 21047	. . . . . . 7 |- ( ph -> ( s e. ( fi ` B ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
52	5, 1, 25, 50	fmfnfmlem3 21049	. . . . . . . . 9 |- ( ph -> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) )
53	52	eleq2d 2534	. . . . . . . 8 |- ( ph -> ( s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> s e. ran ( x e. L |-> ( `' F " x ) ) ) )
54		vex 3034	. . . . . . . . . 10 |- s e. _V
55	31	elrnmpt 5087	. . . . . . . . . 10 |- ( s e. _V -> ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) ) )
56	54, 55	ax-mp 5	. . . . . . . . 9 |- ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) )
57	5, 1, 25, 50	fmfnfmlem2 21048	. . . . . . . . 9 |- ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
58	56, 57	syl5bi 225	. . . . . . . 8 |- ( ph -> ( s e. ran ( x e. L |-> ( `' F " x ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
59	53, 58	sylbid 223	. . . . . . 7 |- ( ph -> ( s e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
60	52	eleq2d 2534	. . . . . . . . . . . . 13 |- ( ph -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> w e. ran ( x e. L |-> ( `' F " x ) ) ) )
61		vex 3034	. . . . . . . . . . . . . 14 |- w e. _V
62	31	elrnmpt 5087	. . . . . . . . . . . . . 14 |- ( w e. _V -> ( w e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L w = ( `' F " x ) ) )
63	61, 62	ax-mp 5	. . . . . . . . . . . . 13 |- ( w e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L w = ( `' F " x ) )
64	60, 63	syl6bb 269	. . . . . . . . . . . 12 |- ( ph -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> E. x e. L w = ( `' F " x ) ) )
65	64	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ z e. ( fi ` B ) ) -> ( w e. ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) <-> E. x e. L w = ( `' F " x ) ) )
66		fbssfi 20930	. . . . . . . . . . . . 13 |- ( ( B e. ( fBas ` Y ) /\ z e. ( fi ` B ) ) -> E. s e. B s C_ z )
67	5, 66	sylan 479	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ( fi ` B ) ) -> E. s e. B s C_ z )
68	1	ad3antrrr 744	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) )
69	1	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( s e. B /\ s C_ z ) ) -> L e. ( Fil ` X ) )
70	50	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ s e. B ) -> ( ( X FilMap F ) ` B ) C_ L )
71		filtop 20948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( L e. ( Fil ` X ) -> X e. L )
72	1, 71	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> X e. L )
73	72, 5, 25	3jca 1210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
74	73	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ s e. B ) -> ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) )
75		ssfg 20965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( B e. ( fBas ` Y ) -> B C_ ( Y filGen B ) )
76	5, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> B C_ ( Y filGen B ) )
77	76	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ s e. B ) -> s e. ( Y filGen B ) )
78		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( Y filGen B ) = ( Y filGen B )
79	78	imaelfm 21044	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ s e. ( Y filGen B ) ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
80	74, 77, 79	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ s e. B ) -> ( F " s ) e. ( ( X FilMap F ) ` B ) )
81	70, 80	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ s e. B ) -> ( F " s ) e. L )
82	81	adantrr 731	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( s e. B /\ s C_ z ) ) -> ( F " s ) e. L )
83	69, 82	jca 541	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( s e. B /\ s C_ z ) ) -> ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) )
84		filin 20947	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
85	84	3expa 1231	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( L e. ( Fil ` X ) /\ ( F " s ) e. L ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
86	83, 85	sylan 479	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> ( ( F " s ) i^i x ) e. L )
87	86	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 )
88		simprr 774	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> t C_ X )
89		elin 3608	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. ( ( F " s ) i^i x ) <-> ( w e. ( F " s ) /\ w e. x ) )
90	25, 36	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> Fun F )
91		fvelima 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Fun F /\ w e. ( F " s ) ) -> E. y e. s ( F ` y ) = w )
92	91	ex 441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( Fun F -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
93	90, 92	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
94	93	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ t C_ X ) -> ( w e. ( F " s ) -> E. y e. s ( F ` y ) = w ) )
95	90	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> Fun F )
96		simplrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> s C_ z )
97		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) -> y e. s )
98		ssel2 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( s C_ z /\ y e. s ) -> y e. z )
99	96, 97, 98	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> y e. z )
100	90	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> Fun F )
101		fbelss 20926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( B e. ( fBas ` Y ) /\ s e. B ) -> s C_ Y )
102	5, 101	sylan 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ s e. B ) -> s C_ Y )
103	27	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ s e. B ) -> dom F = Y )
104	102, 103	sseqtr4d 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ s e. B ) -> s C_ dom F )
105	104	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ ( s e. B /\ s C_ z ) ) -> s C_ dom F )
106	105	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> y e. dom F )
107		fvimacnv 6012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
108	100, 106, 107	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
109	108	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ y e. s ) -> ( ( F ` y ) e. x -> y e. ( `' F " x ) ) )
110	109	impr 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ ( y e. s /\ ( F ` y ) e. x ) ) -> y e. ( `' F " x ) )
111	110	ad2ant2rl 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( t C_ X /\ ( y e. s /\ ( F ` y ) e. x ) ) ) -> y e. ( `' F " x ) )
112	99, 111	elind 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 ) ) )
113		inss2 3644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z i^i ( `' F " x ) ) C_ ( `' F " x )
114		cnvimass 5194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( `' F " x ) C_ dom F
115	113, 114	sstri 3427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z i^i ( `' F " x ) ) C_ dom F
116		funfvima2 6158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 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 ) ) ) ) )
117	115, 116	mpan2 685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( Fun F -> ( y e. ( z i^i ( `' F " x ) ) -> ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) ) )
118	95, 112, 117	sylc 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 ) ) ) )
119	118	anassrs 660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( 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 ) ) ) )
120	119	expr 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( 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 ) ) ) ) )
121		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( F ` y ) = w -> ( ( F ` y ) e. x <-> w e. x ) )
122		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( F ` y ) = w -> ( ( F ` y ) e. ( F " ( z i^i ( `' F " x ) ) ) <-> w e. ( F " ( z i^i ( `' F " x ) ) ) ) )
123	121, 122	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) ) ) ) ) )
124	120, 123	syl5ibcom 228	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( 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 ) ) ) ) ) )
125	124	rexlimdva 2871	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) ) )
126	94, 125	syld 44	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) ) ) ) )
127	126	impd 438	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) ) ) )
128	89, 127	syl5bi 225	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) ) ) )
129	128	adantrl 730	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) ) )
130	129	ssrdv 3424	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) ) ) )
131		simprl 772	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
132	130, 131	sstrd 3428	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 )
133		filss 20946	. . . . . . . . . . . . . . . . . 18 |- ( ( L e. ( Fil ` X ) /\ ( ( ( F " s ) i^i x ) e. L /\ t C_ X /\ ( ( F " s ) i^i x ) C_ t ) ) -> t e. L )
134	68, 87, 88, 132, 133	syl13anc 1294	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) /\ ( ( F " ( z i^i ( `' F " x ) ) ) C_ t /\ t C_ X ) ) -> t e. L )
135	134	exp32 616	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( s e. B /\ s C_ z ) ) /\ x e. L ) -> ( ( F " ( z i^i ( `' F " x ) ) ) C_ t -> ( t C_ X -> t e. L ) ) )
136		ineq2 3619	. . . . . . . . . . . . . . . . . . 19 |- ( w = ( `' F " x ) -> ( z i^i w ) = ( z i^i ( `' F " x ) ) )
137	136	imaeq2d 5174	. . . . . . . . . . . . . . . . . 18 |- ( w = ( `' F " x ) -> ( F " ( z i^i w ) ) = ( F " ( z i^i ( `' F " x ) ) ) )
138	137	sseq1d 3445	. . . . . . . . . . . . . . . . 17 |- ( w = ( `' F " x ) -> ( ( F " ( z i^i w ) ) C_ t <-> ( F " ( z i^i ( `' F " x ) ) ) C_ t ) )
139	138	imbi1d 324	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
140	135, 139	syl5ibrcom 230	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
141	140	rexlimdva 2871	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
142	141	rexlimdvaa 2872	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) )
143	142	imp 436	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
144	67, 143	syldan 478	. . . . . . . . . . 11 |- ( ( 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 ) ) ) )
145	65, 144	sylbid 223	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
146	145	impr 631	. . . . . . . . 9 |- ( ( 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 ) ) )
147		imaeq2 5170	. . . . . . . . . . 11 |- ( s = ( z i^i w ) -> ( F " s ) = ( F " ( z i^i w ) ) )
148	147	sseq1d 3445	. . . . . . . . . 10 |- ( s = ( z i^i w ) -> ( ( F " s ) C_ t <-> ( F " ( z i^i w ) ) C_ t ) )
149	148	imbi1d 324	. . . . . . . . 9 |- ( 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 ) ) ) )
150	146, 149	syl5ibrcom 230	. . . . . . . 8 |- ( ( 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 ) ) ) )
151	150	rexlimdvva 2878	. . . . . . 7 |- ( 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 ) ) ) )
152	51, 59, 151	3jaod 1358	. . . . . 6 |- ( 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 ) ) ) )
153	49, 152	sylbid 223	. . . . 5 |- ( ph -> ( s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
154	153	rexlimdv 2870	. . . 4 |- ( ph -> ( E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) )
155	154	com23 80	. . 3 |- ( ph -> ( t C_ X -> ( E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t -> t e. L ) ) )
156	155	impd 438	. 2 |- ( ph -> ( ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) -> t e. L ) )
157	47, 156	impbid 195	1 |- ( ph -> ( t e. L <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   \/ w3o 1006   /\ w3a 1007   = wceq 1452   e. wcel 1904   E.wrex 2757   _Vcvv 3031   u. cun 3388   i^i cin 3389   C_ wss 3390   |-> cmpt 4454   `'ccnv 4838   dom cdm 4839   ran crn 4840   "cima 4842   Fun wfun 5583   -->wf 5585   ` cfv 5589  (class class class)co 6308   ficfi 7942   fBascfbas 19035   filGencfg 19036   Filcfil 20938   FilMap cfm 21026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-fin 7591  df-fi 7943  df-fbas 19044  df-fg 19045  df-fil 20939  df-fm 21031

This theorem is referenced by:  fmfnfm  21051