Theorem fmfnfmlem4 15597

Description: Lemma for fmfnfm 15598.

Hypotheses

Ref	Expression
fmfnfm.1	|- Y = U.B
fmfnfm.2	|- Z = U.L

Assertion

Ref	Expression
fmfnfmlem4	|- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t e. L <-> (t C_ X /\ E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t)))

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

Proof of Theorem fmfnfmlem4

Step	Hyp	Ref	Expression
1		elssuni 3206	. . . . . . 7 |- (t e. L -> t C_ U.L)
2		fmfnfm.2	. . . . . . 7 |- Z = U.L
3	1, 2	syl6ssr 2664	. . . . . 6 |- (t e. L -> t C_ Z)
4	3	ad2antll 443	. . . . 5 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> t C_ Z)
5		simpl3 881	. . . . 5 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> X = Z)
6	4, 5	sseqtr4d 2654	. . . 4 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> t C_ X)
7	6	expr 418	. . 3 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t e. L -> t C_ X))
8		ssun2 2768	. . . . . . . 8 |- {y | E.x e. L y = (`'F"x)} C_ (B u. {y | E.x e. L y = (`'F"x)})
9	8	a1i 8	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> {y | E.x e. L y = (`'F"x)} C_ (B u. {y | E.x e. L y = (`'F"x)}))
10		unexg 3798	. . . . . . . . . . . 12 |- ((B e. fBas /\ {y | E.x e. L y = (`'F"x)} e. _V) -> (B u. {y | E.x e. L y = (`'F"x)}) e. _V)
11		abrexexg 4837	. . . . . . . . . . . 12 |- (L e. Fil -> {y | E.x e. L y = (`'F"x)} e. _V)
12	10, 11	sylan2 500	. . . . . . . . . . 11 |- ((B e. fBas /\ L e. Fil) -> (B u. {y | E.x e. L y = (`'F"x)}) e. _V)
13	12	3adant3 896	. . . . . . . . . 10 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> (B u. {y | E.x e. L y = (`'F"x)}) e. _V)
14	13	3ad2ant1 897	. . . . . . . . 9 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (B u. {y | E.x e. L y = (`'F"x)}) e. _V)
15	14	adantr 425	. . . . . . . 8 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> (B u. {y | E.x e. L y = (`'F"x)}) e. _V)
16		abfi2 10216	. . . . . . . 8 |- ((B u. {y | E.x e. L y = (`'F"x)}) e. _V -> (B u. {y | E.x e. L y = (`'F"x)}) C_ ( fi ` (B u. {y | E.x e. L y = (`'F"x)})))
17	15, 16	syl 12	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> (B u. {y | E.x e. L y = (`'F"x)}) C_ ( fi ` (B u. {y | E.x e. L y = (`'F"x)})))
18	9, 17	sstrd 2627	. . . . . 6 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> {y | E.x e. L y = (`'F"x)} C_ ( fi ` (B u. {y | E.x e. L y = (`'F"x)})))
19		eqid 1884	. . . . . . . . 9 |- (`'F"t) = (`'F"t)
20		imaeq2 4260	. . . . . . . . . . 11 |- (x = t -> (`'F"x) = (`'F"t))
21	20	eqeq2d 1895	. . . . . . . . . 10 |- (x = t -> ((`'F"t) = (`'F"x) <-> (`'F"t) = (`'F"t)))
22	21	rcla4ev 2381	. . . . . . . . 9 |- ((t e. L /\ (`'F"t) = (`'F"t)) -> E.x e. L (`'F"t) = (`'F"x))
23	19, 22	mpan2 760	. . . . . . . 8 |- (t e. L -> E.x e. L (`'F"t) = (`'F"x))
24	23	ad2antll 443	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> E.x e. L (`'F"t) = (`'F"x))
25		cnvimass 4286	. . . . . . . . . . . . . 14 |- (`'F"t) C_ dom F
26	25	a1i 8	. . . . . . . . . . . . 13 |- ((B e. fBas /\ F:Y-->X) -> (`'F"t) C_ dom F)
27		fdm 4567	. . . . . . . . . . . . . 14 |- (F:Y-->X -> dom F = Y)
28	27	adantl 424	. . . . . . . . . . . . 13 |- ((B e. fBas /\ F:Y-->X) -> dom F = Y)
29	26, 28	sseqtrd 2653	. . . . . . . . . . . 12 |- ((B e. fBas /\ F:Y-->X) -> (`'F"t) C_ Y)
30		uniexg 3795	. . . . . . . . . . . . . 14 |- (B e. fBas -> U.B e. _V)
31		fmfnfm.1	. . . . . . . . . . . . . 14 |- Y = U.B
32	30, 31	syl5eqel 1975	. . . . . . . . . . . . 13 |- (B e. fBas -> Y e. _V)
33	32	adantr 425	. . . . . . . . . . . 12 |- ((B e. fBas /\ F:Y-->X) -> Y e. _V)
34		ssexg 3457	. . . . . . . . . . . 12 |- (((`'F"t) C_ Y /\ Y e. _V) -> (`'F"t) e. _V)
35	29, 33, 34	syl11anc 524	. . . . . . . . . . 11 |- ((B e. fBas /\ F:Y-->X) -> (`'F"t) e. _V)
36		eqeq1 1890	. . . . . . . . . . . . 13 |- (y = (`'F"t) -> (y = (`'F"x) <-> (`'F"t) = (`'F"x)))
37	36	rexbidv 2124	. . . . . . . . . . . 12 |- (y = (`'F"t) -> (E.x e. L y = (`'F"x) <-> E.x e. L (`'F"t) = (`'F"x)))
38	37	elabg 2405	. . . . . . . . . . 11 |- ((`'F"t) e. _V -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
39	35, 38	syl 12	. . . . . . . . . 10 |- ((B e. fBas /\ F:Y-->X) -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
40	39	3adant2 895	. . . . . . . . 9 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
41	40	3ad2ant1 897	. . . . . . . 8 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> ((`'F"t) e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L (`'F"t) = (`'F"x)))
42	41	adantr 425	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B 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)))
43	24, 42	mpbird 213	. . . . . 6 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> (`'F"t) e. {y | E.x e. L y = (`'F"x)})
44	18, 43	sseldd 2620	. . . . 5 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> (`'F"t) e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)})))
45		ffun 4565	. . . . . . . . 9 |- (F:Y-->X -> Fun F)
46		ssid 2634	. . . . . . . . . 10 |- (`'F"t) C_ (`'F"t)
47		funimass2 4492	. . . . . . . . . 10 |- ((Fun F /\ (`'F"t) C_ (`'F"t)) -> (F"(`'F"t)) C_ t)
48	46, 47	mpan2 760	. . . . . . . . 9 |- (Fun F -> (F"(`'F"t)) C_ t)
49	45, 48	syl 12	. . . . . . . 8 |- (F:Y-->X -> (F"(`'F"t)) C_ t)
50	49	3ad2ant3 899	. . . . . . 7 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> (F"(`'F"t)) C_ t)
51	50	3ad2ant1 897	. . . . . 6 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (F"(`'F"t)) C_ t)
52	51	adantr 425	. . . . 5 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> (F"(`'F"t)) C_ t)
53		imaeq2 4260	. . . . . . 7 |- (s = (`'F"t) -> (F"s) = (F"(`'F"t)))
54	53	sseq1d 2644	. . . . . 6 |- (s = (`'F"t) -> ((F"s) C_ t <-> (F"(`'F"t)) C_ t))
55	54	rcla4ev 2381	. . . . 5 |- (((`'F"t) e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ (F"(`'F"t)) C_ t) -> E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t)
56	44, 52, 55	syl11anc 524	. . . 4 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)})) /\ t e. L)) -> E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t)
57	56	expr 418	. . 3 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t e. L -> E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t))
58	7, 57	jcad 661	. 2 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t e. L -> (t C_ X /\ E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t)))
59		simpl11 951	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> B e. fBas)
60	11	3ad2ant2 898	. . . . . . . . 9 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> {y | E.x e. L y = (`'F"x)} e. _V)
61	60	3ad2ant1 897	. . . . . . . 8 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> {y | E.x e. L y = (`'F"x)} e. _V)
62	61	adantr 425	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> {y | E.x e. L y = (`'F"x)} e. _V)
63		elfiun 15369	. . . . . . 7 |- ((B e. fBas /\ {y | E.x e. L y = (`'F"x)} e. _V) -> (s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)})) <-> (s e. ( fi ` B) \/ s e. ( fi ` {y | E.x e. L y = (`'F"x)}) \/ E.u e. ( fi ` B)E.v e. ( fi ` {y | E.x e. L y = (`'F"x)})s = (u i^i v))))
64	59, 62, 63	syl11anc 524	. . . . . 6 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)})) <-> (s e. ( fi ` B) \/ s e. ( fi ` {y | E.x e. L y = (`'F"x)}) \/ E.u e. ( fi ` B)E.v e. ( fi ` {y | E.x e. L y = (`'F"x)})s = (u i^i v))))
65	31, 2	fmfnfmlem1 15594	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (s e. ( fi ` B) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
66	31, 2	fmfnfmlem3 15596	. . . . . . . . 9 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> ( fi ` {y | E.x e. L y = (`'F"x)}) = {y | E.x e. L y = (`'F"x)})
67	66	eleq2d 1964	. . . . . . . 8 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (s e. ( fi ` {y | E.x e. L y = (`'F"x)}) <-> s e. {y | E.x e. L y = (`'F"x)}))
68	31, 2	fmfnfmlem2 15595	. . . . . . . . 9 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (E.x e. L s = (`'F"x) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
69		visset 2295	. . . . . . . . . 10 |- s e. _V
70		eqeq1 1890	. . . . . . . . . . 11 |- (y = s -> (y = (`'F"x) <-> s = (`'F"x)))
71	70	rexbidv 2124	. . . . . . . . . 10 |- (y = s -> (E.x e. L y = (`'F"x) <-> E.x e. L s = (`'F"x)))
72	69, 71	elab 2403	. . . . . . . . 9 |- (s e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L s = (`'F"x))
73	68, 72	syl5ib 223	. . . . . . . 8 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B 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))))
74	67, 73	sylbid 220	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (s e. ( fi ` {y | E.x e. L y = (`'F"x)}) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
75	66	eleq2d 1964	. . . . . . . . . . 11 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (v e. ( fi ` {y | E.x e. L y = (`'F"x)}) <-> v e. {y | E.x e. L y = (`'F"x)}))
76		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- u e. _V
77		sppfi 10218	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. _V /\ B e. fBas) -> (u e. ( fi ` B) <-> E.y(y C_ B /\ y e. Fin /\ u = |^|y)))
78	76, 77	mpan 759	. . . . . . . . . . . . . . . . . . 19 |- (B e. fBas -> (u e. ( fi ` B) <-> E.y(y C_ B /\ y e. Fin /\ u = |^|y)))
79	78	3ad2ant1 897	. . . . . . . . . . . . . . . . . 18 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> (u e. ( fi ` B) <-> E.y(y C_ B /\ y e. Fin /\ u = |^|y)))
80	79	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (u e. ( fi ` B) <-> E.y(y C_ B /\ y e. Fin /\ u = |^|y)))
81	80	adantr 425	. . . . . . . . . . . . . . . 16 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (u e. ( fi ` B) <-> E.y(y C_ B /\ y e. Fin /\ u = |^|y)))
82		fbssint 10279	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. fBas /\ y C_ B /\ y e. Fin) -> E.z e. B z C_ |^|y)
83	82	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . 23 |- (B e. fBas -> ((y C_ B /\ y e. Fin) -> E.z e. B z C_ |^|y))
84	83	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> ((y C_ B /\ y e. Fin) -> E.z e. B z C_ |^|y))
85	84	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . 21 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> ((y C_ B /\ y e. Fin) -> E.z e. B z C_ |^|y))
86	85	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> ((y C_ B /\ y e. Fin) -> E.z e. B z C_ |^|y))
87		simpl12 952	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> L e. Fil)
88	87	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> L e. Fil)
89		simpll2 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) -> ((X FilMap B)` F) C_ L)
90		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L e. Fil /\ X = Z) -> X = Z)
91	2	filusb 10267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (L e. Fil -> Z e. L)
92	91	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((L e. Fil /\ X = Z) -> Z e. L)
93	90, 92	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((L e. Fil /\ X = Z) -> X e. L)
94	93	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ X = Z) -> X e. L)
95	94	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> X e. L)
96	95	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) -> X e. L)
97		simpl11 951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) -> B e. fBas)
98		simpl13 953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) -> F:Y-->X)
99		fbssfg 10285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (B e. fBas -> B C_ (filGen` B))
100	99	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> B C_ (filGen` B))
101	100	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> B C_ (filGen` B))
102	101	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (z e. B -> z e. (filGen` B)))
103	102	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) -> z e. (filGen` B))
104		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (filGen` B) = (filGen` B)
105	31, 104	imaelfm 15591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((X e. L /\ B e. fBas /\ F:Y-->X) /\ z e. (filGen` B)) -> (F"z) e. ((X FilMap B)` F))
106	96, 97, 98, 103, 105	syl31anc 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) -> (F"z) e. ((X FilMap B)` F))
107	106	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) -> (F"z) e. ((X FilMap B)` F))
108	89, 107	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) -> (F"z) e. L)
109	108	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (F"z) e. L)
110		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> x e. L)
111	110	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> x e. L)
112		filint 10269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((L e. Fil /\ (F"z) e. L /\ x e. L) -> ((F"z) i^i x) e. L)
113	88, 109, 111, 112	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> ((F"z) i^i x) e. L)
114		simpl3 881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> X = Z)
115	114	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ (F"s) C_ t)) -> X = Z)
116	115	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ (F"s) C_ t)) -> (t C_ X <-> t C_ Z))
117	116	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ (F"s) C_ t)) -> (t C_ X -> t C_ Z))
118	117	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (z C_ u /\ s = (u i^i v))) -> ((F"s) C_ t -> (t C_ X -> t C_ Z)))
119	118	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (z C_ u /\ s = (u i^i v))) -> (((F"s) C_ t /\ t C_ X) -> t C_ Z))
120	119	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> t C_ Z)
121		fvelima 4723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((Fun F /\ w e. (F"z)) -> E.y e. z (F` y) = w)
122	121	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (Fun F -> (w e. (F"z) -> E.y e. z (F` y) = w))
123	45, 122	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (F:Y-->X -> (w e. (F"z) -> E.y e. z (F` y) = w))
124	123	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> (w e. (F"z) -> E.y e. z (F` y) = w))
125	124	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (w e. (F"z) -> E.y e. z (F` y) = w))
126	125	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (w e. (F"z) -> E.y e. z (F` y) = w))
127	126	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (w e. (F"z) -> E.y e. z (F` y) = w))
128		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F` y) = w -> ((F` y) e. x <-> w e. x))
129		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F` y) = w -> ((F` y) e. (F"s) <-> w e. (F"s)))
130	128, 129	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((F` y) = w -> (((F` y) e. x -> (F` y) e. (F"s)) <-> (w e. x -> w e. (F"s))))
131	45	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((B e. fBas /\ L e. Fil /\ F:Y-->X) -> Fun F)
132	131	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> Fun F)
133	132	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> Fun F)
134	133	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> Fun F)
135		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((z C_ Y /\ y e. z) -> y e. Y)
136		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (z e. B -> z C_ U.B)
137	136, 31	syl6ssr 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (z e. B -> z C_ Y)
138	135, 137	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((z e. B /\ y e. z) -> y e. Y)
139	138	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((F:Y-->X /\ (z e. B /\ y e. z)) -> y e. Y)
140	27	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((F:Y-->X /\ (z e. B /\ y e. z)) -> dom F = Y)
141	139, 140	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((F:Y-->X /\ (z e. B /\ y e. z)) -> y e. dom F)
142	141	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ (z e. B /\ y e. z)) -> y e. dom F)
143	142	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (z e. B /\ y e. z)) -> y e. dom F)
144	143	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ z e. B) /\ y e. z) -> y e. dom F)
145	144	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ y e. z) -> y e. dom F)
146	145	adantrl 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> y e. dom F)
147		fvimacnv 4778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((Fun F /\ y e. dom F) -> ((F` y) e. x <-> y e. (`'F"x)))
148	134, 146, 147	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> ((F` y) e. x <-> y e. (`'F"x)))
149	133	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> Fun F)
150		inss2 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (u i^i v) C_ v
151	150	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> (u i^i v) C_ v)
152		simpllr 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) -> s = (u i^i v))
153	152	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> s = (u i^i v))
154		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> v = (`'F"x))
155	154	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> v = (`'F"x))
156	155	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> (`'F"x) = v)
157	151, 153, 156	3sstr4d 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> s C_ (`'F"x))
158		cnvimass 4286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (`'F"x) C_ dom F
159	158	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> (`'F"x) C_ dom F)
160	157, 159	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> s C_ dom F)
161	149, 160	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> (Fun F /\ s C_ dom F))
162		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y e. (u i^i v) <-> (y e. u /\ y e. v))
163		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) -> z C_ u)
164	163	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) -> (y e. z -> y e. u))
165	164	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) -> y e. u)
166	165	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> y e. u)
167	154	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> v = (`'F"x))
168	167	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> (y e. v <-> y e. (`'F"x)))
169	168	biimprd 171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> (y e. (`'F"x) -> y e. v))
170	169	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> y e. v)
171	162, 166, 170	sylanbrc 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> y e. (u i^i v))
172	171, 153	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> y e. s)
173		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((Fun F /\ s C_ dom F) -> (y e. s -> (F` y) e. (F"s)))
174	161, 172, 173	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z) /\ y e. (`'F"x))) -> (F` y) e. (F"s))
175	174	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> (y e. (`'F"x) -> (F` y) e. (F"s)))
176	148, 175	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> ((F` y) e. x -> (F` y) e. (F"s)))
177	130, 176	syl5cbi 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X)) /\ y e. z)) -> ((F` y) = w -> (w e. x -> w e. (F"s))))
178	177	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (y e. z -> ((F` y) = w -> (w e. x -> w e. (F"s)))))
179	178	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (E.y e. z (F` y) = w -> (w e. x -> w e. (F"s))))
180	127, 179	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (w e. (F"z) -> (w e. x -> w e. (F"s))))
181	180	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> ((w e. (F"z) /\ w e. x) -> w e. (F"s)))
182		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w e. ((F"z) i^i x) <-> (w e. (F"z) /\ w e. x))
183	181, 182	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (w e. ((F"z) i^i x) -> w e. (F"s)))
184	183	ssrdv 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> ((F"z) i^i x) C_ (F"s))
185		simprrl 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (F"s) C_ t)
186	184, 185	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> ((F"z) i^i x) C_ t)
187	113, 120, 186	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> (((F"z) i^i x) e. L /\ t C_ Z /\ ((F"z) i^i x) C_ t))
188	2	fillsb 10270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (L e. Fil -> ((((F"z) i^i x) e. L /\ t C_ Z /\ ((F"z) i^i x) C_ t) -> t e. L))
189	88, 187, 188	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ ((z C_ u /\ s = (u i^i v)) /\ ((F"s) C_ t /\ t C_ X))) -> t e. L)
190	189	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (z C_ u /\ s = (u i^i v))) -> (((F"s) C_ t /\ t C_ X) -> t e. L))
191	190	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) /\ z e. B) /\ (z C_ u /\ s = (u i^i v))) -> ((F"s) C_ t -> (t C_ X -> t e. L)))
192	191	exp43 415	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (z e. B -> (z C_ u -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
193		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = |^|y -> (z C_ u <-> z C_ |^|y))
194	193	biimparc 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z C_ |^|y /\ u = |^|y) -> z C_ u)
195	192, 194	syl7 26	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (z e. B -> ((z C_ |^|y /\ u = |^|y) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
196	195	exp4a 409	. . . . . . . . . . . . . . . . . . . . 21 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (z e. B -> (z C_ |^|y -> (u = |^|y -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))))
197	196	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . 20 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (E.z e. B z C_ |^|y -> (u = |^|y -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
198	86, 197	syld 30	. . . . . . . . . . . . . . . . . . 19 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> ((y C_ B /\ y e. Fin) -> (u = |^|y -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
199	198	exp3a 405	. . . . . . . . . . . . . . . . . 18 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (y C_ B -> (y e. Fin -> (u = |^|y -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))))
200	199	3impd 1082	. . . . . . . . . . . . . . . . 17 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> ((y C_ B /\ y e. Fin /\ u = |^|y) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))
201	200	19.23adv 1584	. . . . . . . . . . . . . . . 16 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (E.y(y C_ B /\ y e. Fin /\ u = |^|y) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))
202	81, 201	sylbid 220	. . . . . . . . . . . . . . 15 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ (x e. L /\ v = (`'F"x))) -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))
203	202	exp32 408	. . . . . . . . . . . . . 14 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (x e. L -> (v = (`'F"x) -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))))
204	203	r19.23adv 2215	. . . . . . . . . . . . 13 |- (((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) -> (E.x e. L v = (`'F"x) -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
205	204	adantr 425	. . . . . . . . . . . 12 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (E.x e. L v = (`'F"x) -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
206		visset 2295	. . . . . . . . . . . . 13 |- v e. _V
207		eqeq1 1890	. . . . . . . . . . . . . 14 |- (y = v -> (y = (`'F"x) <-> v = (`'F"x)))
208	207	rexbidv 2124	. . . . . . . . . . . . 13 |- (y = v -> (E.x e. L y = (`'F"x) <-> E.x e. L v = (`'F"x)))
209	206, 208	elab 2403	. . . . . . . . . . . 12 |- (v e. {y | E.x e. L y = (`'F"x)} <-> E.x e. L v = (`'F"x))
210	205, 209	syl5ib 223	. . . . . . . . . . 11 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (v e. {y | E.x e. L y = (`'F"x)} -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
211	75, 210	sylbid 220	. . . . . . . . . 10 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (v e. ( fi ` {y | E.x e. L y = (`'F"x)}) -> (u e. ( fi ` B) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
212	211	com23 36	. . . . . . . . 9 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (u e. ( fi ` B) -> (v e. ( fi ` {y | E.x e. L y = (`'F"x)}) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))))
213	212	imp3a 388	. . . . . . . 8 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> ((u e. ( fi ` B) /\ v e. ( fi ` {y | E.x e. L y = (`'F"x)})) -> (s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L)))))
214	213	r19.23advv 2218	. . . . . . 7 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (E.u e. ( fi ` B)E.v e. ( fi ` {y | E.x e. L y = (`'F"x)})s = (u i^i v) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
215	65, 74, 214	3jaod 1161	. . . . . 6 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> ((s e. ( fi ` B) \/ s e. ( fi ` {y | E.x e. L y = (`'F"x)}) \/ E.u e. ( fi ` B)E.v e. ( fi ` {y | E.x e. L y = (`'F"x)})s = (u i^i v)) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
216	64, 215	sylbid 220	. . . . 5 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)})) -> ((F"s) C_ t -> (t C_ X -> t e. L))))
217	216	r19.23adv 2215	. . . 4 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t -> (t C_ X -> t e. L)))
218	217	com23 36	. . 3 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t C_ X -> (E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t -> t e. L)))
219	218	imp3a 388	. 2 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> ((t C_ X /\ E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t) -> t e. L))
220	58, 219	impbid 574	1 |- ((((B e. fBas /\ L e. Fil /\ F:Y-->X) /\ ((X FilMap B)` F) C_ L /\ X = Z) /\ Y = U.( fi ` (B u. {y | E.x e. L y = (`'F"x)}))) -> (t e. L <-> (t C_ X /\ E.s e. ( fi ` (B u. {y | E.x e. L y = (`'F"x)}))(F"s) C_ t)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  U.cuni 3177  |^|cint 3214  `'ccnv 3985  dom cdm 3986  "cima 3989  Fun wfun 3992  -->wf 3994  ` cfv 3998  (class class class)co 4884  Fincfn 5426   fi cfi 10210  fBascfbas 10257  filGencfg 10258  Filcfil 10264   FilMap cfilmap 10304

This theorem is referenced by:  fmfnfm 15598

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-3or 859  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-reu 2111  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-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-map 5383  df-en 5427  df-fin 5430  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-filmap 10306

Copyright terms: Public domain