Theorem f1lindf 18231

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)

Assertion

Ref	Expression
f1lindf	|- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF W )

Proof of Theorem f1lindf

Dummy variables k x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2438	. . . . . . 7 |- ( Base ` W ) = ( Base ` W )
2	1	lindff 18224	. . . . . 6 |- ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> ( Base ` W ) )
3	2	ancoms 453	. . . . 5 |- ( ( W e. LMod /\ F LIndF W ) -> F : dom F --> ( Base ` W ) )
4	3	3adant3 1008	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5		f1f 5601	. . . . 5 |- ( G : K -1-1-> dom F -> G : K --> dom F )
6	5	3ad2ant3 1011	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7		fco 5563	. . . 4 |- ( ( F : dom F --> ( Base ` W ) /\ G : K --> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
8	4, 6, 7	syl2anc 661	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
9		ffdm 5567	. . . 4 |- ( ( F o. G ) : K --> ( Base ` W ) -> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ dom ( F o. G ) C_ K ) )
10	9	simpld 459	. . 3 |- ( ( F o. G ) : K --> ( Base ` W ) -> ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) )
11	8, 10	syl 16	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) )
12		simpl2 992	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> F LIndF W )
13	6	adantr 465	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G : K --> dom F )
14		fdm 5558	. . . . . . . . . 10 |- ( ( F o. G ) : K --> ( Base ` W ) -> dom ( F o. G ) = K )
15	8, 14	syl 16	. . . . . . . . 9 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom ( F o. G ) = K )
16	15	eleq2d 2505	. . . . . . . 8 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( x e. dom ( F o. G ) <-> x e. K ) )
17	16	biimpa 484	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> x e. K )
18	13, 17	ffvelrnd 5839	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( G ` x ) e. dom F )
19	18	adantrr 716	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> ( G ` x ) e. dom F )
20		eldifi 3473	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k e. ( Base ` (Scalar ` W ) ) )
21	20	ad2antll 728	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> k e. ( Base ` (Scalar ` W ) ) )
22		eldifsni 3996	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k =/= ( 0g ` (Scalar ` W ) ) )
23	22	ad2antll 728	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> k =/= ( 0g ` (Scalar ` W ) ) )
24		eqid 2438	. . . . . 6 |- ( .s ` W ) = ( .s ` W )
25		eqid 2438	. . . . . 6 |- ( LSpan ` W ) = ( LSpan ` W )
26		eqid 2438	. . . . . 6 |- (Scalar ` W ) = (Scalar ` W )
27		eqid 2438	. . . . . 6 |- ( 0g ` (Scalar ` W ) ) = ( 0g ` (Scalar ` W ) )
28		eqid 2438	. . . . . 6 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
29	24, 25, 26, 27, 28	lindfind 18225	. . . . 5 |- ( ( ( F LIndF W /\ ( G ` x ) e. dom F ) /\ ( k e. ( Base ` (Scalar ` W ) ) /\ k =/= ( 0g ` (Scalar ` W ) ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
30	12, 19, 21, 23, 29	syl22anc 1219	. . . 4 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
31		f1fn 5602	. . . . . . . . . . 11 |- ( G : K -1-1-> dom F -> G Fn K )
32	31	3ad2ant3 1011	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G Fn K )
33	32	adantr 465	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G Fn K )
34		fvco2 5761	. . . . . . . . 9 |- ( ( G Fn K /\ x e. K ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
35	33, 17, 34	syl2anc 661	. . . . . . . 8 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
36	35	oveq2d 6102	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( k ( .s ` W ) ( ( F o. G ) ` x ) ) = ( k ( .s ` W ) ( F ` ( G ` x ) ) ) )
37	36	eleq1d 2504	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) <-> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) )
38		simpl1 991	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
39		imassrn 5175	. . . . . . . . . . 11 |- ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
40		frn 5560	. . . . . . . . . . . 12 |- ( F : dom F --> ( Base ` W ) -> ran F C_ ( Base ` W ) )
41	4, 40	syl 16	. . . . . . . . . . 11 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ran F C_ ( Base ` W ) )
42	39, 41	syl5ss 3362	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
43	42	adantr 465	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
44		imaco 5338	. . . . . . . . . 10 |- ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
45	15	difeq1d 3468	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
46	45	imaeq2d 5164	. . . . . . . . . . . . . 14 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( G " ( K \ { x } ) ) )
47		df-f1 5418	. . . . . . . . . . . . . . . . 17 |- ( G : K -1-1-> dom F <-> ( G : K --> dom F /\ Fun `' G ) )
48	47	simprbi 464	. . . . . . . . . . . . . . . 16 |- ( G : K -1-1-> dom F -> Fun `' G )
49	48	3ad2ant3 1011	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
50		imadif 5488	. . . . . . . . . . . . . . 15 |- ( Fun `' G -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
51	49, 50	syl 16	. . . . . . . . . . . . . 14 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
52	46, 51	eqtrd 2470	. . . . . . . . . . . . 13 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
53	52	adantr 465	. . . . . . . . . . . 12 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
54		fnsnfv 5746	. . . . . . . . . . . . . . 15 |- ( ( G Fn K /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
55	32, 54	sylan 471	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
56	55	difeq2d 3469	. . . . . . . . . . . . 13 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) = ( ( G " K ) \ ( G " { x } ) ) )
57		imassrn 5175	. . . . . . . . . . . . . . 15 |- ( G " K ) C_ ran G
58	6	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> G : K --> dom F )
59		frn 5560	. . . . . . . . . . . . . . . 16 |- ( G : K --> dom F -> ran G C_ dom F )
60	58, 59	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ran G C_ dom F )
61	57, 60	syl5ss 3362	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
62	61	ssdifd 3487	. . . . . . . . . . . . 13 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) C_ ( dom F \ { ( G ` x ) } ) )
63	56, 62	eqsstr3d 3386	. . . . . . . . . . . 12 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ ( G " { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
64	53, 63	eqsstrd 3385	. . . . . . . . . . 11 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
65		imass2 5199	. . . . . . . . . . 11 |- ( ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
66	64, 65	syl 16	. . . . . . . . . 10 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
67	44, 66	syl5eqss 3395	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
68	1, 25	lspss 17045	. . . . . . . . 9 |- ( ( W e. LMod /\ ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) /\ ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
69	38, 43, 67, 68	syl3anc 1218	. . . . . . . 8 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
70	17, 69	syldan 470	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
71	70	sseld 3350	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
72	37, 71	sylbid 215	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
73	72	adantrr 716	. . . 4 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
74	30, 73	mtod 177	. . 3 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
75	74	ralrimivva 2803	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
76		simp1 988	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
77		rellindf 18217	. . . . . 6 |- Rel LIndF
78	77	brrelexi 4874	. . . . 5 |- ( F LIndF W -> F e. _V )
79	78	3ad2ant2 1010	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
80		simp3 990	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
81		dmexg 6504	. . . . . . 7 |- ( F e. _V -> dom F e. _V )
82	79, 81	syl 16	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom F e. _V )
83		f1dmex 6542	. . . . . 6 |- ( ( G : K -1-1-> dom F /\ dom F e. _V ) -> K e. _V )
84	80, 82, 83	syl2anc 661	. . . . 5 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> K e. _V )
85		fex 5945	. . . . 5 |- ( ( G : K --> dom F /\ K e. _V ) -> G e. _V )
86	6, 84, 85	syl2anc 661	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G e. _V )
87		coexg 6523	. . . 4 |- ( ( F e. _V /\ G e. _V ) -> ( F o. G ) e. _V )
88	79, 86, 87	syl2anc 661	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) e. _V )
89	1, 24, 25, 26, 28, 27	islindf 18221	. . 3 |- ( ( W e. LMod /\ ( F o. G ) e. _V ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
90	76, 88, 89	syl2anc 661	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
91	11, 75, 90	mpbir2and 913	1 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF W )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2601   A.wral 2710   _Vcvv 2967   \ cdif 3320   C_ wss 3323   {csn 3872   class class class wbr 4287   `'ccnv 4834   dom cdm 4835   ran crn 4836   "cima 4838   o. ccom 4839   Fun wfun 5407   Fn wfn 5408   -->wf 5409   -1-1->wf1 5410   ` cfv 5413  (class class class)co 6086   Basecbs 14166  Scalarcsca 14233   .scvsca 14234   0gc0g 14370   LModclmod 16928   LSpanclspn 17032   LIndF clindf 18213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-slot 14170  df-base 14171  df-0g 14372  df-mnd 15407  df-grp 15536  df-lmod 16930  df-lss 16994  df-lsp 17033  df-lindf 18215

This theorem is referenced by:  lindfres  18232  f1linds  18234