Theorem f1lindf 18724

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 2441	. . . . . . 7 |- ( Base ` W ) = ( Base ` W )
2	1	lindff 18717	. . . . . 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 1015	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5		f1f 5767	. . . . 5 |- ( G : K -1-1-> dom F -> G : K --> dom F )
6	5	3ad2ant3 1018	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7		fco 5727	. . . 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 5731	. . . 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 999	. . . . 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 5721	. . . . . . . . . 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 2511	. . . . . . . 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 3608	. . . . . 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 4137	. . . . . 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 2441	. . . . . 6 |- ( .s ` W ) = ( .s ` W )
25		eqid 2441	. . . . . 6 |- ( LSpan ` W ) = ( LSpan ` W )
26		eqid 2441	. . . . . 6 |- (Scalar ` W ) = (Scalar ` W )
27		eqid 2441	. . . . . 6 |- ( 0g ` (Scalar ` W ) ) = ( 0g ` (Scalar ` W ) )
28		eqid 2441	. . . . . 6 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
29	24, 25, 26, 27, 28	lindfind 18718	. . . . 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 1228	. . . 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 5768	. . . . . . . . . . 11 |- ( G : K -1-1-> dom F -> G Fn K )
32	31	3ad2ant3 1018	. . . . . . . . . 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 5929	. . . . . . . . 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 6293	. . . . . . 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 2510	. . . . . 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 998	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
39		imassrn 5334	. . . . . . . . . . 11 |- ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
40		frn 5723	. . . . . . . . . . . 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 3497	. . . . . . . . . 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 5498	. . . . . . . . . 10 |- ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
45	15	difeq1d 3603	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
46	45	imaeq2d 5323	. . . . . . . . . . . . . 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 5579	. . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
50		imadif 5649	. . . . . . . . . . . . . . 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 2482	. . . . . . . . . . . . 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 5914	. . . . . . . . . . . . . . 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 3604	. . . . . . . . . . . . 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 5334	. . . . . . . . . . . . . . 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 5723	. . . . . . . . . . . . . . . 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 3497	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
62	61	ssdifd 3622	. . . . . . . . . . . . 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 3521	. . . . . . . . . . . 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 3520	. . . . . . . . . . 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 5358	. . . . . . . . . . 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 3530	. . . . . . . . 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 17498	. . . . . . . . 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 1227	. . . . . . . 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 3485	. . . . . 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 2862	. 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 995	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
77		rellindf 18710	. . . . . 6 |- Rel LIndF
78	77	brrelexi 5026	. . . . 5 |- ( F LIndF W -> F e. _V )
79	78	3ad2ant2 1017	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
80		simp3 997	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
81		dmexg 6712	. . . . . . 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 6751	. . . . . 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 6126	. . . . 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 6732	. . . 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 18714	. . 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 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 369   /\ w3a 972   = wceq 1381   e. wcel 1802   =/= wne 2636   A.wral 2791   _Vcvv 3093   \ cdif 3455   C_ wss 3458   {csn 4010   class class class wbr 4433   `'ccnv 4984   dom cdm 4985   ran crn 4986   "cima 4988   o. ccom 4989   Fun wfun 5568   Fn wfn 5569   -->wf 5570   -1-1->wf1 5571   ` cfv 5574  (class class class)co 6277   Basecbs 14504  Scalarcsca 14572   .scvsca 14573   0gc0g 14709   LModclmod 17380   LSpanclspn 17485   LIndF clindf 18706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-slot 14508  df-base 14509  df-0g 14711  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-grp 15926  df-lmod 17382  df-lss 17447  df-lsp 17486  df-lindf 18708

This theorem is referenced by:  lindfres  18725  f1linds  18727