Theorem f1lindf 18617

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 2460	. . . . . . 7 |- ( Base ` W ) = ( Base ` W )
2	1	lindff 18610	. . . . . 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 1011	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5		f1f 5772	. . . . 5 |- ( G : K -1-1-> dom F -> G : K --> dom F )
6	5	3ad2ant3 1014	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7		fco 5732	. . . 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 5736	. . . 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 995	. . . . 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 5726	. . . . . . . . . 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 2530	. . . . . . . 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 6013	. . . . . 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 3619	. . . . . 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 4146	. . . . . 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 2460	. . . . . 6 |- ( .s ` W ) = ( .s ` W )
25		eqid 2460	. . . . . 6 |- ( LSpan ` W ) = ( LSpan ` W )
26		eqid 2460	. . . . . 6 |- (Scalar ` W ) = (Scalar ` W )
27		eqid 2460	. . . . . 6 |- ( 0g ` (Scalar ` W ) ) = ( 0g ` (Scalar ` W ) )
28		eqid 2460	. . . . . 6 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
29	24, 25, 26, 27, 28	lindfind 18611	. . . . 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 1224	. . . 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 5773	. . . . . . . . . . 11 |- ( G : K -1-1-> dom F -> G Fn K )
32	31	3ad2ant3 1014	. . . . . . . . . 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 5933	. . . . . . . . 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 6291	. . . . . . 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 2529	. . . . . 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 994	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
39		imassrn 5339	. . . . . . . . . . 11 |- ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
40		frn 5728	. . . . . . . . . . . 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 3508	. . . . . . . . . 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 5503	. . . . . . . . . 10 |- ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
45	15	difeq1d 3614	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
46	45	imaeq2d 5328	. . . . . . . . . . . . . 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 5584	. . . . . . . . . . . . . . . . 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 1014	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
50		imadif 5654	. . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . 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 5918	. . . . . . . . . . . . . . 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 3615	. . . . . . . . . . . . 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 5339	. . . . . . . . . . . . . . 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 5728	. . . . . . . . . . . . . . . 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 3508	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
62	61	ssdifd 3633	. . . . . . . . . . . . 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 3532	. . . . . . . . . . . 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 3531	. . . . . . . . . . 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 5363	. . . . . . . . . . 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 3541	. . . . . . . . 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 17406	. . . . . . . . 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 1223	. . . . . . . 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 3496	. . . . . 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 2878	. 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 991	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
77		rellindf 18603	. . . . . 6 |- Rel LIndF
78	77	brrelexi 5032	. . . . 5 |- ( F LIndF W -> F e. _V )
79	78	3ad2ant2 1013	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
80		simp3 993	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
81		dmexg 6705	. . . . . . 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 6744	. . . . . 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 6124	. . . . 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 6725	. . . 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 18607	. . 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 915	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 968   = wceq 1374   e. wcel 1762   =/= wne 2655   A.wral 2807   _Vcvv 3106   \ cdif 3466   C_ wss 3469   {csn 4020   class class class wbr 4440   `'ccnv 4991   dom cdm 4992   ran crn 4993   "cima 4995   o. ccom 4996   Fun wfun 5573   Fn wfn 5574   -->wf 5575   -1-1->wf1 5576   ` cfv 5579  (class class class)co 6275   Basecbs 14479  Scalarcsca 14547   .scvsca 14548   0gc0g 14684   LModclmod 17288   LSpanclspn 17393   LIndF clindf 18599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-slot 14483  df-base 14484  df-0g 14686  df-mnd 15721  df-grp 15851  df-lmod 17290  df-lss 17355  df-lsp 17394  df-lindf 18601

This theorem is referenced by:  lindfres  18618  f1linds  18620