Theorem f1lindf 18942

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 2382	. . . . . . 7 |- ( Base ` W ) = ( Base ` W )
2	1	lindff 18935	. . . . . 6 |- ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> ( Base ` W ) )
3	2	ancoms 451	. . . . 5 |- ( ( W e. LMod /\ F LIndF W ) -> F : dom F --> ( Base ` W ) )
4	3	3adant3 1014	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5		f1f 5689	. . . . 5 |- ( G : K -1-1-> dom F -> G : K --> dom F )
6	5	3ad2ant3 1017	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7		fco 5649	. . . 4 |- ( ( F : dom F --> ( Base ` W ) /\ G : K --> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
8	4, 6, 7	syl2anc 659	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
9		ffdm 5653	. . . 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 457	. . 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 998	. . . . 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 463	. . . . . . 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 5643	. . . . . . . . . 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 2452	. . . . . . . 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 482	. . . . . . 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 5934	. . . . . 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 714	. . . . 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 3540	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k e. ( Base ` (Scalar ` W ) ) )
21	20	ad2antll 726	. . . . 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 4070	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k =/= ( 0g ` (Scalar ` W ) ) )
23	22	ad2antll 726	. . . . 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 2382	. . . . . 6 |- ( .s ` W ) = ( .s ` W )
25		eqid 2382	. . . . . 6 |- ( LSpan ` W ) = ( LSpan ` W )
26		eqid 2382	. . . . . 6 |- (Scalar ` W ) = (Scalar ` W )
27		eqid 2382	. . . . . 6 |- ( 0g ` (Scalar ` W ) ) = ( 0g ` (Scalar ` W ) )
28		eqid 2382	. . . . . 6 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
29	24, 25, 26, 27, 28	lindfind 18936	. . . . 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 1227	. . . 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 5690	. . . . . . . . . . 11 |- ( G : K -1-1-> dom F -> G Fn K )
32	31	3ad2ant3 1017	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G Fn K )
33	32	adantr 463	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G Fn K )
34		fvco2 5849	. . . . . . . . 9 |- ( ( G Fn K /\ x e. K ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
35	33, 17, 34	syl2anc 659	. . . . . . . 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 6212	. . . . . . 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 2451	. . . . . 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 997	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
39		imassrn 5260	. . . . . . . . . . 11 |- ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
40		frn 5645	. . . . . . . . . . . 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 3428	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
43	42	adantr 463	. . . . . . . . 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 5420	. . . . . . . . . 10 |- ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
45	15	difeq1d 3535	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
46	45	imaeq2d 5249	. . . . . . . . . . . . . 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 5501	. . . . . . . . . . . . . . . . 17 |- ( G : K -1-1-> dom F <-> ( G : K --> dom F /\ Fun `' G ) )
48	47	simprbi 462	. . . . . . . . . . . . . . . 16 |- ( G : K -1-1-> dom F -> Fun `' G )
49	48	3ad2ant3 1017	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
50		imadif 5571	. . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . 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 463	. . . . . . . . . . . 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 5834	. . . . . . . . . . . . . . 15 |- ( ( G Fn K /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
55	32, 54	sylan 469	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
56	55	difeq2d 3536	. . . . . . . . . . . . 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 5260	. . . . . . . . . . . . . . 15 |- ( G " K ) C_ ran G
58	6	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> G : K --> dom F )
59		frn 5645	. . . . . . . . . . . . . . . 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 3428	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
62	61	ssdifd 3554	. . . . . . . . . . . . 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 3452	. . . . . . . . . . . 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 3451	. . . . . . . . . . 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 5284	. . . . . . . . . . 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 3461	. . . . . . . . 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 17743	. . . . . . . . 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 1226	. . . . . . . 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 468	. . . . . . 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 3416	. . . . . 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 714	. . . 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 994	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
77		rellindf 18928	. . . . . 6 |- Rel LIndF
78	77	brrelexi 4954	. . . . 5 |- ( F LIndF W -> F e. _V )
79	78	3ad2ant2 1016	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
80		simp3 996	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
81		dmexg 6630	. . . . . . 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 6669	. . . . . 6 |- ( ( G : K -1-1-> dom F /\ dom F e. _V ) -> K e. _V )
84	80, 82, 83	syl2anc 659	. . . . 5 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> K e. _V )
85		fex 6046	. . . . 5 |- ( ( G : K --> dom F /\ K e. _V ) -> G e. _V )
86	6, 84, 85	syl2anc 659	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G e. _V )
87		coexg 6650	. . . 4 |- ( ( F e. _V /\ G e. _V ) -> ( F o. G ) e. _V )
88	79, 86, 87	syl2anc 659	. . 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 18932	. . 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 659	. 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 920	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 367   /\ w3a 971   = wceq 1399   e. wcel 1826   =/= wne 2577   A.wral 2732   _Vcvv 3034   \ cdif 3386   C_ wss 3389   {csn 3944   class class class wbr 4367   `'ccnv 4912   dom cdm 4913   ran crn 4914   "cima 4916   o. ccom 4917   Fun wfun 5490   Fn wfn 5491   -->wf 5492   -1-1->wf1 5493   ` cfv 5496  (class class class)co 6196   Basecbs 14634  Scalarcsca 14705   .scvsca 14706   0gc0g 14847   LModclmod 17625   LSpanclspn 17730   LIndF clindf 18924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-slot 14638  df-base 14639  df-0g 14849  df-mgm 15989  df-sgrp 16028  df-mnd 16038  df-grp 16174  df-lmod 17627  df-lss 17692  df-lsp 17731  df-lindf 18926

This theorem is referenced by:  lindfres  18943  f1linds  18945