Theorem rnelfm 15593

Description: A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-NoV-2009.)

Hypothesis

Ref	Expression
rnelfm.1	|- X = U.L

Assertion

Ref	Expression
rnelfm	|- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F)) <-> ran F e. L))

Distinct variable groups:   A,b   F,b   L,b   X,b   Y,b

Proof of Theorem rnelfm

Step	Hyp	Ref	Expression
1		eleq2 1958	. . . . . . . 8 |- (L = ((X FilMap b)` F) -> (ran F e. L <-> ran F e. ((X FilMap b)` F)))
2		ffn 4562	. . . . . . . . . . . 12 |- (F:Y-->X -> F Fn Y)
3		dffn4 4623	. . . . . . . . . . . 12 |- (F Fn Y <-> F:Y-onto->ran F)
4	2, 3	sylib 215	. . . . . . . . . . 11 |- (F:Y-->X -> F:Y-onto->ran F)
5		foima 4622	. . . . . . . . . . 11 |- (F:Y-onto->ran F -> (F"Y) = ran F)
6	4, 5	syl 12	. . . . . . . . . 10 |- (F:Y-->X -> (F"Y) = ran F)
7	6	ad2antlr 441	. . . . . . . . 9 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> (F"Y) = ran F)
8		simpll 448	. . . . . . . . . 10 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> X e. L)
9		simprl 450	. . . . . . . . . 10 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> b e. fBas)
10		feq2 4552	. . . . . . . . . . . 12 |- (Y = U.b -> (F:Y-->X <-> F:U.b-->X))
11	10	biimpac 462	. . . . . . . . . . 11 |- ((F:Y-->X /\ Y = U.b) -> F:U.b-->X)
12	11	ad2ant2l 444	. . . . . . . . . 10 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> F:U.b-->X)
13		simpr 350	. . . . . . . . . . . . 13 |- ((b e. fBas /\ Y = U.b) -> Y = U.b)
14		eqid 1884	. . . . . . . . . . . . . . 15 |- U.b = U.b
15	14	fgbas 10286	. . . . . . . . . . . . . 14 |- (b e. fBas -> U.b = U.(filGen` b))
16	15	adantr 425	. . . . . . . . . . . . 13 |- ((b e. fBas /\ Y = U.b) -> U.b = U.(filGen` b))
17	13, 16	eqtrd 1925	. . . . . . . . . . . 12 |- ((b e. fBas /\ Y = U.b) -> Y = U.(filGen` b))
18	17	adantl 424	. . . . . . . . . . 11 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> Y = U.(filGen` b))
19		fgfil 10290	. . . . . . . . . . . . 13 |- (b e. fBas -> (filGen` b) e. Fil)
20		eqid 1884	. . . . . . . . . . . . . 14 |- U.(filGen` b) = U.(filGen` b)
21	20	filusb 10267	. . . . . . . . . . . . 13 |- ((filGen` b) e. Fil -> U.(filGen` b) e. (filGen` b))
22	19, 21	syl 12	. . . . . . . . . . . 12 |- (b e. fBas -> U.(filGen` b) e. (filGen` b))
23	22	ad2antrl 442	. . . . . . . . . . 11 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> U.(filGen` b) e. (filGen` b))
24	18, 23	eqeltrd 1971	. . . . . . . . . 10 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> Y e. (filGen` b))
25		eqid 1884	. . . . . . . . . . 11 |- (filGen` b) = (filGen` b)
26	14, 25	imaelfm 15591	. . . . . . . . . 10 |- (((X e. L /\ b e. fBas /\ F:U.b-->X) /\ Y e. (filGen` b)) -> (F"Y) e. ((X FilMap b)` F))
27	8, 9, 12, 24, 26	syl31anc 1103	. . . . . . . . 9 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> (F"Y) e. ((X FilMap b)` F))
28	7, 27	eqeltrrd 1972	. . . . . . . 8 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> ran F e. ((X FilMap b)` F))
29	1, 28	syl5cbir 228	. . . . . . 7 |- (((X e. L /\ F:Y-->X) /\ (b e. fBas /\ Y = U.b)) -> (L = ((X FilMap b)` F) -> ran F e. L))
30	29	exp32 408	. . . . . 6 |- ((X e. L /\ F:Y-->X) -> (b e. fBas -> (Y = U.b -> (L = ((X FilMap b)` F) -> ran F e. L))))
31	30	imp4a 391	. . . . 5 |- ((X e. L /\ F:Y-->X) -> (b e. fBas -> ((Y = U.b /\ L = ((X FilMap b)` F)) -> ran F e. L)))
32		rnelfm.1	. . . . . 6 |- X = U.L
33	32	filusb 10267	. . . . 5 |- (L e. Fil -> X e. L)
34	31, 33	sylan 497	. . . 4 |- ((L e. Fil /\ F:Y-->X) -> (b e. fBas -> ((Y = U.b /\ L = ((X FilMap b)` F)) -> ran F e. L)))
35	34	3adant1 894	. . 3 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (b e. fBas -> ((Y = U.b /\ L = ((X FilMap b)` F)) -> ran F e. L)))
36	35	r19.23adv 2215	. 2 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F)) -> ran F e. L))
37	32	rnelfmlem 15592	. . . 4 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> {y | E.x e. L y = (`'F"x)} e. fBas)
38	33	3ad2ant2 898	. . . . . . . . . 10 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> X e. L)
39	38	adantr 425	. . . . . . . . 9 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> X e. L)
40		fimacnv 4783	. . . . . . . . . . . 12 |- (F:Y-->X -> (`'F"X) = Y)
41	40	eqcomd 1889	. . . . . . . . . . 11 |- (F:Y-->X -> Y = (`'F"X))
42	41	3ad2ant3 899	. . . . . . . . . 10 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> Y = (`'F"X))
43	42	adantr 425	. . . . . . . . 9 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Y = (`'F"X))
44		imaeq2 4260	. . . . . . . . . . 11 |- (x = X -> (`'F"x) = (`'F"X))
45	44	eqeq2d 1895	. . . . . . . . . 10 |- (x = X -> (Y = (`'F"x) <-> Y = (`'F"X)))
46	45	rcla4ev 2381	. . . . . . . . 9 |- ((X e. L /\ Y = (`'F"X)) -> E.x e. L Y = (`'F"x))
47	39, 43, 46	syl11anc 524	. . . . . . . 8 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> E.x e. L Y = (`'F"x))
48		eqeq1 1890	. . . . . . . . . . . 12 |- (y = Y -> (y = (`'F"x) <-> Y = (`'F"x)))
49	48	rexbidv 2124	. . . . . . . . . . 11 |- (y = Y -> (E.x e. L y = (`'F"x) <-> E.x e. L Y = (`'F"x)))
50	49	elabg 2405	. . . . . . . . . 10 |- (Y e. A -> (Y e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L Y = (`'F"x)))
51	50	3ad2ant1 897	. . . . . . . . 9 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (Y e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L Y = (`'F"x)))
52	51	adantr 425	. . . . . . . 8 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (Y e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L Y = (`'F"x)))
53	47, 52	mpbird 213	. . . . . . 7 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Y e. {y | E.x e. L y = (`'F"x)})
54		elssuni 3206	. . . . . . 7 |- (Y e. {y | E.x e. L y = (`'F"x)} -> Y C_ U.{y | E.x e. L y = (`'F"x)})
55	53, 54	syl 12	. . . . . 6 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Y C_ U.{y | E.x e. L y = (`'F"x)})
56		sseq1 2637	. . . . . . . . . . . 12 |- (z = (`'F"x) -> (z C_ Y <-> (`'F"x) C_ Y))
57		cnvimass 4286	. . . . . . . . . . . . . . . 16 |- (`'F"x) C_ dom F
58	57	a1i 8	. . . . . . . . . . . . . . 15 |- (F:Y-->X -> (`'F"x) C_ dom F)
59		fdm 4567	. . . . . . . . . . . . . . 15 |- (F:Y-->X -> dom F = Y)
60	58, 59	sseqtrd 2653	. . . . . . . . . . . . . 14 |- (F:Y-->X -> (`'F"x) C_ Y)
61	60	3ad2ant3 899	. . . . . . . . . . . . 13 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (`'F"x) C_ Y)
62	61	adantr 425	. . . . . . . . . . . 12 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (`'F"x) C_ Y)
63	56, 62	syl5cbir 228	. . . . . . . . . . 11 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (z = (`'F"x) -> z C_ Y))
64	63	a1d 15	. . . . . . . . . 10 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (x e. L -> (z = (`'F"x) -> z C_ Y)))
65	64	r19.23adv 2215	. . . . . . . . 9 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (E.x e. L z = (`'F"x) -> z C_ Y))
66		visset 2295	. . . . . . . . . 10 |- z e. _V
67		eqeq1 1890	. . . . . . . . . . 11 |- (y = z -> (y = (`'F"x) <-> z = (`'F"x)))
68	67	rexbidv 2124	. . . . . . . . . 10 |- (y = z -> (E.x e. L y = (`'F"x) <-> E.x e. L z = (`'F"x)))
69	66, 68	elab 2403	. . . . . . . . 9 |- (z e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L z = (`'F"x))
70	65, 69	syl5ib 223	. . . . . . . 8 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (z e. {y | E.x e. L y = (`'F"x)} -> z C_ Y))
71	70	r19.21aiv 2175	. . . . . . 7 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> A.z e. {y | E.x e. L y = (`'F"x)}z C_ Y)
72		unissb 3208	. . . . . . 7 |- (U.{y | E.x e. L y = (`'F"x)} C_ Y <-> A.z e. {y | E.x e. L y = (`'F"x)}z C_ Y)
73	71, 72	sylibr 217	. . . . . 6 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> U.{y | E.x e. L y = (`'F"x)} C_ Y)
74	55, 73	eqssd 2633	. . . . 5 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Y = U.{y | E.x e. L y = (`'F"x)})
75		elssuni 3206	. . . . . . . . . . . 12 |- (t e. L -> t C_ U.L)
76	75, 32	syl6ssr 2664	. . . . . . . . . . 11 |- (t e. L -> t C_ X)
77	76	a1i 8	. . . . . . . . . 10 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. L -> t C_ X))
78		simprr 451	. . . . . . . . . . . . . 14 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> t e. L)
79		eqidd 1885	. . . . . . . . . . . . . 14 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> (`'F"t) = (`'F"t))
80		imaeq2 4260	. . . . . . . . . . . . . . . 16 |- (x = t -> (`'F"x) = (`'F"t))
81	80	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (x = t -> ((`'F"t) = (`'F"x) <-> (`'F"t) = (`'F"t)))
82	81	rcla4ev 2381	. . . . . . . . . . . . . 14 |- ((t e. L /\ (`'F"t) = (`'F"t)) -> E.x e. L (`'F"t) = (`'F"x))
83	78, 79, 82	syl11anc 524	. . . . . . . . . . . . 13 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> E.x e. L (`'F"t) = (`'F"x))
84		cnvimass 4286	. . . . . . . . . . . . . . . . . . . 20 |- (`'F"t) C_ dom F
85	84	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (F:Y-->X -> (`'F"t) C_ dom F)
86	85, 59	sseqtrd 2653	. . . . . . . . . . . . . . . . . 18 |- (F:Y-->X -> (`'F"t) C_ Y)
87	86	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (`'F"t) C_ Y)
88	87	adantr 425	. . . . . . . . . . . . . . . 16 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (`'F"t) C_ Y)
89		simpl1 879	. . . . . . . . . . . . . . . 16 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Y e. A)
90		ssexg 3457	. . . . . . . . . . . . . . . 16 |- (((`'F"t) C_ Y /\ Y e. A) -> (`'F"t) e. _V)
91	88, 89, 90	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (`'F"t) e. _V)
92		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (y = (`'F"t) -> (y = (`'F"x) <-> (`'F"t) = (`'F"x)))
93	92	rexbidv 2124	. . . . . . . . . . . . . . . 16 |- (y = (`'F"t) -> (E.x e. L y = (`'F"x) <-> E.x e. L (`'F"t) = (`'F"x)))
94	93	elabg 2405	. . . . . . . . . . . . . . 15 |- ((`'F"t) e. _V -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
95	91, 94	syl 12	. . . . . . . . . . . . . 14 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
96	95	adantr 425	. . . . . . . . . . . . 13 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
97	83, 96	mpbird 213	. . . . . . . . . . . 12 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> (`'F"t) e. {y | E.x e. L y = (`'F"x)})
98		ssid 2634	. . . . . . . . . . . . 13 |- (`'F"t) C_ (`'F"t)
99		ffun 4565	. . . . . . . . . . . . . . . 16 |- (F:Y-->X -> Fun F)
100	99	3ad2ant3 899	. . . . . . . . . . . . . . 15 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> Fun F)
101	100	ad2antrr 440	. . . . . . . . . . . . . 14 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> Fun F)
102	84	a1i 8	. . . . . . . . . . . . . 14 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> (`'F"t) C_ dom F)
103		funimass3 4779	. . . . . . . . . . . . . 14 |- ((Fun F /\ (`'F"t) C_ dom F) -> ((F"(`'F"t)) C_ t <-> (`'F"t) C_ (`'F"t)))
104	101, 102, 103	syl11anc 524	. . . . . . . . . . . . 13 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> ((F"(`'F"t)) C_ t <-> (`'F"t) C_ (`'F"t)))
105	98, 104	mpbiri 211	. . . . . . . . . . . 12 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> (F"(`'F"t)) C_ t)
106		imaeq2 4260	. . . . . . . . . . . . . 14 |- (s = (`'F"t) -> (F"s) = (F"(`'F"t)))
107	106	sseq1d 2644	. . . . . . . . . . . . 13 |- (s = (`'F"t) -> ((F"s) C_ t <-> (F"(`'F"t)) C_ t))
108	107	rcla4ev 2381	. . . . . . . . . . . 12 |- (((`'F"t) e. {y | E.x e. L y = (`'F"x)} /\ (F"(`'F"t)) C_ t) -> E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)
109	97, 105, 108	syl11anc 524	. . . . . . . . . . 11 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ t e. L)) -> E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)
110	109	expr 418	. . . . . . . . . 10 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. L -> E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t))
111	77, 110	jcad 661	. . . . . . . . 9 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. L -> (t C_ X /\ E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)))
112		simpl2 880	. . . . . . . . . . . . . . 15 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> L e. Fil)
113	112	ad2antrr 440	. . . . . . . . . . . . . 14 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> L e. Fil)
114		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = (`'F"x) -> (F"s) = (F"(`'F"x)))
115	114	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (`'F"x) -> ((F"s) C_ t <-> (F"(`'F"x)) C_ t))
116	114	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = (`'F"x) -> ((F"s) e. L <-> (F"(`'F"x)) e. L))
117	116	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (`'F"x) -> ((t C_ X -> (F"s) e. L) <-> (t C_ X -> (F"(`'F"x)) e. L)))
118	115, 117	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (s = (`'F"x) -> (((F"s) C_ t -> (t C_ X -> (F"s) e. L)) <-> ((F"(`'F"x)) C_ t -> (t C_ X -> (F"(`'F"x)) e. L))))
119		ssid 2634	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'F"x) C_ (`'F"x)
120	100	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> Fun F)
121	120	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> Fun F)
122	57	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (`'F"x) C_ dom F)
123		funimass3 4779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Fun F /\ (`'F"x) C_ dom F) -> ((F"(`'F"x)) C_ x <-> (`'F"x) C_ (`'F"x)))
124	121, 122, 123	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> ((F"(`'F"x)) C_ x <-> (`'F"x) C_ (`'F"x)))
125	119, 124	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (F"(`'F"x)) C_ x)
126		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F"(`'F"x)) C_ ran F
127	125, 126	jctir 317	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> ((F"(`'F"x)) C_ x /\ (F"(`'F"x)) C_ ran F))
128		ssin 2814	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F"(`'F"x)) C_ x /\ (F"(`'F"x)) C_ ran F) <-> (F"(`'F"x)) C_ (x i^i ran F))
129	127, 128	sylib 215	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (F"(`'F"x)) C_ (x i^i ran F))
130		fvelrnb 4719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (F Fn Y -> (z e. ran F <-> E.y e. Y (F` y) = z))
131	2, 130	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (F:Y-->X -> (z e. ran F <-> E.y e. Y (F` y) = z))
132	131	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (z e. ran F <-> E.y e. Y (F` y) = z))
133	132	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (z e. ran F <-> E.y e. Y (F` y) = z))
134	133	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (z e. ran F <-> E.y e. Y (F` y) = z))
135		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F` y) = z -> ((F` y) e. x <-> z e. x))
136		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F` y) = z -> ((F` y) e. (F"(`'F"x)) <-> z e. (F"(`'F"x))))
137	135, 136	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F` y) = z -> (((F` y) e. x -> (F` y) e. (F"(`'F"x))) <-> (z e. x -> z e. (F"(`'F"x)))))
138	121	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) /\ (F` y) e. x) -> Fun F)
139	138, 57	jctir 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) /\ (F` y) e. x) -> (Fun F /\ (`'F"x) C_ dom F))
140	100	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) -> Fun F)
141	140	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) -> Fun F)
142	59	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> dom F = Y)
143	142	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> dom F = Y)
144	143	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> dom F = Y)
145	144	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (y e. dom F <-> y e. Y))
146	145	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) -> y e. dom F)
147		fvimacnv 4778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((Fun F /\ y e. dom F) -> ((F` y) e. x <-> y e. (`'F"x)))
148	141, 146, 147	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) -> ((F` y) e. x <-> y e. (`'F"x)))
149	148	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) /\ (F` y) e. x) -> y e. (`'F"x))
150		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((Fun F /\ (`'F"x) C_ dom F) -> (y e. (`'F"x) -> (F` y) e. (F"(`'F"x))))
151	139, 149, 150	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) /\ (F` y) e. x) -> (F` y) e. (F"(`'F"x)))
152	151	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) -> ((F` y) e. x -> (F` y) e. (F"(`'F"x))))
153	137, 152	syl5cbi 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) /\ y e. Y) -> ((F` y) = z -> (z e. x -> z e. (F"(`'F"x)))))
154	153	r19.23adva 2216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (E.y e. Y (F` y) = z -> (z e. x -> z e. (F"(`'F"x)))))
155	134, 154	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (z e. ran F -> (z e. x -> z e. (F"(`'F"x)))))
156	155	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (z e. x -> (z e. ran F -> z e. (F"(`'F"x)))))
157	156	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> ((z e. x /\ z e. ran F) -> z e. (F"(`'F"x))))
158		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. (x i^i ran F) <-> (z e. x /\ z e. ran F))
159	157, 158	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (z e. (x i^i ran F) -> z e. (F"(`'F"x))))
160	159	ssrdv 2622	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (x i^i ran F) C_ (F"(`'F"x)))
161	129, 160	eqssd 2633	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (F"(`'F"x)) = (x i^i ran F))
162		filint 10269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((L e. Fil /\ x e. L /\ ran F e. L) -> (x i^i ran F) e. L)
163	162	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (L e. Fil -> (x e. L -> (ran F e. L -> (x i^i ran F) e. L)))
164	163	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (L e. Fil -> (ran F e. L -> (x e. L -> (x i^i ran F) e. L)))
165	164	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (ran F e. L -> (x e. L -> (x i^i ran F) e. L)))
166	165	imp31 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) -> (x i^i ran F) e. L)
167	166	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (x i^i ran F) e. L)
168	161, 167	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . 21 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) /\ ((F"(`'F"x)) C_ t /\ t C_ X)) -> (F"(`'F"x)) e. L)
169	168	exp32 408	. . . . . . . . . . . . . . . . . . . 20 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) -> ((F"(`'F"x)) C_ t -> (t C_ X -> (F"(`'F"x)) e. L)))
170	118, 169	syl5cbir 228	. . . . . . . . . . . . . . . . . . 19 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ x e. L) -> (s = (`'F"x) -> ((F"s) C_ t -> (t C_ X -> (F"s) e. L))))
171	170	r19.23adva 2216	. . . . . . . . . . . . . . . . . 18 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (E.x e. L s = (`'F"x) -> ((F"s) C_ t -> (t C_ X -> (F"s) e. L))))
172	171	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (E.x e. L s = (`'F"x) -> ((F"s) C_ t -> (t C_ X -> (F"s) e. L))))
173		visset 2295	. . . . . . . . . . . . . . . . . 18 |- s e. _V
174		eqeq1 1890	. . . . . . . . . . . . . . . . . . 19 |- (y = s -> (y = (`'F"x) <-> s = (`'F"x)))
175	174	rexbidv 2124	. . . . . . . . . . . . . . . . . 18 |- (y = s -> (E.x e. L y = (`'F"x) <-> E.x e. L s = (`'F"x)))
176	173, 175	elab 2403	. . . . . . . . . . . . . . . . 17 |- (s e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L s = (`'F"x))
177	172, 176	syl5ib 223	. . . . . . . . . . . . . . . 16 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (s e. {y | E.x e. L y = (`'F"x)} -> ((F"s) C_ t -> (t C_ X -> (F"s) e. L))))
178	177	imp44 398	. . . . . . . . . . . . . . 15 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> (F"s) e. L)
179		simprr 451	. . . . . . . . . . . . . . 15 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> t C_ X)
180		simprlr 457	. . . . . . . . . . . . . . 15 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> (F"s) C_ t)
181	178, 179, 180	3jca 1050	. . . . . . . . . . . . . 14 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> ((F"s) e. L /\ t C_ X /\ (F"s) C_ t))
182	32	fillsb 10270	. . . . . . . . . . . . . 14 |- (L e. Fil -> (((F"s) e. L /\ t C_ X /\ (F"s) C_ t) -> t e. L))
183	113, 181, 182	sylc 83	. . . . . . . . . . . . 13 |- (((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) /\ ((s e. {y | E.x e. L y = (`'F"x)} /\ (F"s) C_ t) /\ t C_ X)) -> t e. L)
184	183	exp44 416	. . . . . . . . . . . 12 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (s e. {y | E.x e. L y = (`'F"x)} -> ((F"s) C_ t -> (t C_ X -> t e. L))))
185	184	r19.23adv 2215	. . . . . . . . . . 11 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t -> (t C_ X -> t e. L)))
186	185	com23 36	. . . . . . . . . 10 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t C_ X -> (E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t -> t e. L)))
187	186	imp3a 388	. . . . . . . . 9 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> ((t C_ X /\ E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t) -> t e. L))
188	111, 187	impbid 574	. . . . . . . 8 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. L <-> (t C_ X /\ E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)))
189	38	ad2antrr 440	. . . . . . . . 9 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> X e. L)
190	37	adantr 425	. . . . . . . . 9 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> {y | E.x e. L y = (`'F"x)} e. fBas)
191		feq2 4552	. . . . . . . . . . 11 |- (Y = U.{y | E.x e. L y = (`'F"x)} -> (F:Y-->X <-> F:U.{y | E.x e. L y = (`'F"x)}-->X))
192		simpl3 881	. . . . . . . . . . 11 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> F:Y-->X)
193	191, 192	syl5cbi 226	. . . . . . . . . 10 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (Y = U.{y | E.x e. L y = (`'F"x)} -> F:U.{y | E.x e. L y = (`'F"x)}-->X))
194	193	imp 377	. . . . . . . . 9 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> F:U.{y | E.x e. L y = (`'F"x)}-->X)
195		eqid 1884	. . . . . . . . . 10 |- U.{y | E.x e. L y = (`'F"x)} = U.{y | E.x e. L y = (`'F"x)}
196	195	elfilmap 10312	. . . . . . . . 9 |- ((X e. L /\ {y | E.x e. L y = (`'F"x)} e. fBas /\ F:U.{y | E.x e. L y = (`'F"x)}-->X) -> (t e. ((X FilMap {y | E.x e. L y = (`'F"x)})` F) <-> (t C_ X /\ E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)))
197	189, 190, 194, 196	syl111anc 1100	. . . . . . . 8 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. ((X FilMap {y | E.x e. L y = (`'F"x)})` F) <-> (t C_ X /\ E.s e. {y | E.x e. L y = (`'F"x)} (F"s) C_ t)))
198	188, 197	bitr4d 590	. . . . . . 7 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> (t e. L <-> t e. ((X FilMap {y | E.x e. L y = (`'F"x)})` F)))
199	198	eqrdv 1882	. . . . . 6 |- ((((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) /\ Y = U.{y | E.x e. L y = (`'F"x)}) -> L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F))
200	199	ex 402	. . . . 5 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (Y = U.{y | E.x e. L y = (`'F"x)} -> L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F)))
201	74, 200	jcai 313	. . . 4 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> (Y = U.{y | E.x e. L y = (`'F"x)} /\ L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F)))
202		unieq 3185	. . . . . . 7 |- (b = {y | E.x e. L y = (`'F"x)} -> U.b = U.{y | E.x e. L y = (`'F"x)})
203	202	eqeq2d 1895	. . . . . 6 |- (b = {y | E.x e. L y = (`'F"x)} -> (Y = U.b <-> Y = U.{y | E.x e. L y = (`'F"x)}))
204		opreq2 4890	. . . . . . . 8 |- (b = {y | E.x e. L y = (`'F"x)} -> (X FilMap b) = (X FilMap {y | E.x e. L y = (`'F"x)}))
205	204	fveq1d 4683	. . . . . . 7 |- (b = {y | E.x e. L y = (`'F"x)} -> ((X FilMap b)` F) = ((X FilMap {y | E.x e. L y = (`'F"x)})` F))
206	205	eqeq2d 1895	. . . . . 6 |- (b = {y | E.x e. L y = (`'F"x)} -> (L = ((X FilMap b)` F) <-> L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F)))
207	203, 206	anbi12d 690	. . . . 5 |- (b = {y | E.x e. L y = (`'F"x)} -> ((Y = U.b /\ L = ((X FilMap b)` F)) <-> (Y = U.{y | E.x e. L y = (`'F"x)} /\ L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F))))
208	207	rcla4ev 2381	. . . 4 |- (({y | E.x e. L y = (`'F"x)} e. fBas /\ (Y = U.{y | E.x e. L y = (`'F"x)} /\ L = ((X FilMap {y | E.x e. L y = (`'F"x)})` F))) -> E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F)))
209	37, 201, 208	syl11anc 524	. . 3 |- (((Y e. A /\ L e. Fil /\ F:Y-->X) /\ ran F e. L) -> E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F)))
210	209	ex 402	. 2 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (ran F e. L -> E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F))))
211	36, 210	impbid 574	1 |- ((Y e. A /\ L e. Fil /\ F:Y-->X) -> (E.b e. fBas (Y = U.b /\ L = ((X FilMap b)` F)) <-> ran F e. L))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  U.cuni 3177  `'ccnv 3985  dom cdm 3986  ran crn 3987  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  fBascfbas 10257  filGencfg 10258  Filcfil 10264   FilMap cfilmap 10304

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-fbas 10259  df-fg 10260  df-fil 10265  df-filmap 10306

Copyright terms: Public domain