P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	harinf 37601	The Hartogs number of an infinite set is at least om. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ( S e. V /\ -. S e. Fin ) -> om C_ (har ` S ) )
Theorem	wdom2d2 37602*	Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. A ) -> E. y e. B E. z e. C x = X )   =>    |- ( ph -> A ~<_* ( B X. C ) )
Theorem	ttac 37603	Tarski's theorem about choice: infxpidm 9384 is equivalent to ax-ac 9281. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.)
|- (CHOICE <-> A. c ( om ~<_ c -> ( c X. c ) ~~ c ) )
Theorem	pw2f1ocnv 37604*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8067, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( A e. V -> ( F : ( 2o ^m A ) -1-1-onto-> ~P A /\ `' F = ( y e. ~P A |-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )
Theorem	pw2f1o2 37605*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8067, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> ~P A )
Theorem	pw2f1o2val 37606*	Function value of the pw2f1o2 37605 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( X e. ( 2o ^m A ) -> ( F ` X ) = ( `' X " { 1o } ) )
Theorem	pw2f1o2val2 37607*	Membership in a mapped set under the pw2f1o2 37605 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( F ` X ) <-> ( X ` Y ) = 1o ) )
Theorem	soeq12d 37608	Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R Or A <-> S Or B ) )
Theorem	freq12d 37609	Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R Fr A <-> S Fr B ) )
Theorem	weeq12d 37610	Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R We A <-> S We B ) )
Theorem	limsuc2 37611	Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- ( ( Ord A /\ A = U. A ) -> ( B e. A <-> suc B e. A ) )
Theorem	wepwsolem 37612*	Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }   &    |- U = { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }   &    |- F = ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) )   =>    |- ( A e. _V -> F Isom U , T ( ( 2o ^m A ) , ~P A ) )
Theorem	wepwso 37613*	A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove A e. V. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }   =>    |- ( ( A e. V /\ R We A ) -> T Or ~P A )
Theorem	dnnumch1 37614*	Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 8853. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
Theorem	dnnumch2 37615*	Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> A C_ ran F )
Theorem	dnnumch3lem 37616*	Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
Theorem	dnnumch3 37617*	Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On )
Theorem	dnwech 37618*	Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   &    |- H = { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) }   =>    |- ( ph -> H We A )
Theorem	fnwe2val 37619*	Lemma for fnwe2 37623. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   =>    |- ( a T b <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
Theorem	fnwe2lem1 37620*	Lemma for fnwe2 37623. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   =>    |- ( ( ph /\ a e. A ) -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )
Theorem	fnwe2lem2 37621*	Lemma for fnwe2 37623. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus T is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> a C_ A )   &    |- ( ph -> a =/= (/) )   =>    |- ( ph -> E. b e. a A. c e. a -. c T b )
Theorem	fnwe2lem3 37622*	Lemma for fnwe2 37623. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> a e. A )   &    |- ( ph -> b e. A )   =>    |- ( ph -> ( a T b \/ a = b \/ b T a ) )
Theorem	fnwe2 37623*	A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 7293 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   =>    |- ( ph -> T We A )
Theorem	aomclem1 37624*	Lemma for dfac11 37632. This is the beginning of the proof that multiple choice is equivalent to choice. Our goal is to construct, by transfinite recursion, a well-ordering of ( R1 ` A ). In what follows, A is the index of the rank we wish to well-order, z is the collection of well-orderings constructed so far, dom z is the set of ordinal indexes of constructed ranks i.e. the next rank to construct, and y is a postulated multiple-choice function. Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   =>    |- ( ph -> B Or ( R1 ` dom z ) )
Theorem	aomclem2 37625*	Lemma for dfac11 37632. Successor case 2, a choice function for subsets of ( R1 ` dom z ). (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) )
Theorem	aomclem3 37626*	Lemma for dfac11 37632. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E We ( R1 ` dom z ) )
Theorem	aomclem4 37627*	Lemma for dfac11 37632. Limit case. Patch together well-orderings constructed so far using fnwe2 37623 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   =>    |- ( ph -> F We ( R1 ` dom z ) )
Theorem	aomclem5 37628*	Lemma for dfac11 37632. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- ( ph -> dom z e. On )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> G We ( R1 ` dom z ) )
Theorem	aomclem6 37629*	Lemma for dfac11 37632. Transfinite induction, close over z. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- H = recs ( ( z e. _V |-> G ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> ( H ` A ) We ( R1 ` A ) )
Theorem	aomclem7 37630*	Lemma for dfac11 37632. ( R1 ` A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- H = recs ( ( z e. _V |-> G ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E. b b We ( R1 ` A ) )
Theorem	aomclem8 37631*	Lemma for dfac11 37632. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E. b b We ( R1 ` A ) )
Theorem	dfac11 37632*	The right-hand side of this theorem (compare with ac4 9297), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 8497, despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do. This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.)
|- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
Theorem	kelac1 37633*	Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( ph /\ x e. I ) -> S =/= (/) )   &    |- ( ( ph /\ x e. I ) -> J e. Top )   &    |- ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )   &    |- ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )   &    |- ( ( ph /\ x e. I ) -> U e. U. J )   &    |- ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )   =>    |- ( ph -> X_ x e. I S =/= (/) )
Theorem	kelac2lem 37634	Lemma for kelac2 37635 and dfac21 37636: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp )
Theorem	kelac2 37635*	Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( ph /\ x e. I ) -> S e. V )   &    |- ( ( ph /\ x e. I ) -> S =/= (/) )   &    |- ( ph -> ( Xt_ ` ( x e. I |-> ( topGen ` { S , { ~P U. S } } ) ) ) e. Comp )   =>    |- ( ph -> X_ x e. I S =/= (/) )
Theorem	dfac21 37636	Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.)
|- (CHOICE <-> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
20.25.37  Finitely generated left modules
Syntax	clfig 37637	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 37638	Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- LFinGen = { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }
Theorem	islmodfg 37639*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- B = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( W e. LFinGen <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) ) )
Theorem	islssfg 37640*	Property of a finitely generated left (sub-)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) ) )
Theorem	islssfg2 37641*	Property of a finitely generated left (sub-)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- B = ( Base ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ( ~P B i^i Fin ) ( N ` b ) = U ) )
Theorem	islssfgi 37642	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- N = ( LSpan ` W )   &    |- V = ( Base ` W )   &    |- X = ( W ↾s ( N ` B ) )   =>    |- ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> X e. LFinGen )
Theorem	fglmod 37643	Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- ( M e. LFinGen -> M e. LMod )
Theorem	lsmfgcl 37644	The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- U = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- D = ( W ↾s A )   &    |- E = ( W ↾s B )   &    |- F = ( W ↾s ( A .(+) B ) )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. LFinGen )   &    |- ( ph -> E e. LFinGen )   =>    |- ( ph -> F e. LFinGen )
20.25.38  Noetherian left modules I
Syntax	clnm 37645	Extend class notation with the class of Noetherian left modules.
class LNoeM
Definition	df-lnm 37646*	A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- LNoeM = { w e. LMod | A. i e. ( LSubSp ` w ) ( w ↾s i ) e. LFinGen }
Theorem	islnm 37647*	Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- S = ( LSubSp ` M )   =>    |- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S ( M ↾s i ) e. LFinGen ) )
Theorem	islnm2 37648*	Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- B = ( Base ` M )   &    |- S = ( LSubSp ` M )   &    |- N = ( LSpan ` M )   =>    |- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
Theorem	lnmlmod 37649	A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- ( M e. LNoeM -> M e. LMod )
Theorem	lnmlssfg 37650	A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- S = ( LSubSp ` M )   &    |- R = ( M ↾s U )   =>    |- ( ( M e. LNoeM /\ U e. S ) -> R e. LFinGen )
Theorem	lnmlsslnm 37651	All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- S = ( LSubSp ` M )   &    |- R = ( M ↾s U )   =>    |- ( ( M e. LNoeM /\ U e. S ) -> R e. LNoeM )
Theorem	lnmfg 37652	A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
|- ( M e. LNoeM -> M e. LFinGen )
Theorem	kercvrlsm 37653	The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- U = ( LSubSp ` S )   &    |- .(+) = ( LSSum ` S )   &    |- .0. = ( 0g ` T )   &    |- K = ( `' F " { .0. } )   &    |- B = ( Base ` S )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> D e. U )   &    |- ( ph -> ( F " D ) = ran F )   =>    |- ( ph -> ( K .(+) D ) = B )
Theorem	lmhmfgima 37654	A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( T ↾s ( F " A ) )   &    |- X = ( S ↾s A )   &    |- U = ( LSubSp ` S )   &    |- ( ph -> X e. LFinGen )   &    |- ( ph -> A e. U )   &    |- ( ph -> F e. ( S LMHom T ) )   =>    |- ( ph -> Y e. LFinGen )
Theorem	lnmepi 37655	Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- B = ( Base ` T )   =>    |- ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> T e. LNoeM )
Theorem	lmhmfgsplit 37656	If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- .0. = ( 0g ` T )   &    |- K = ( `' F " { .0. } )   &    |- U = ( S ↾s K )   &    |- V = ( T ↾s ran F )   =>    |- ( ( F e. ( S LMHom T ) /\ U e. LFinGen /\ V e. LFinGen ) -> S e. LFinGen )
Theorem	lmhmlnmsplit 37657	If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.)
|- .0. = ( 0g ` T )   &    |- K = ( `' F " { .0. } )   &    |- U = ( S ↾s K )   &    |- V = ( T ↾s ran F )   =>    |- ( ( F e. ( S LMHom T ) /\ U e. LNoeM /\ V e. LNoeM ) -> S e. LNoeM )
Theorem	lnmlmic 37658	Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( R ~=ph𝑚 S -> ( R e. LNoeM <-> S e. LNoeM ) )
20.25.39  Addenda for structure powers
Theorem	pwssplit4 37659*	Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- E = ( R ^s ( A u. B ) )   &    |- G = ( Base ` E )   &    |- .0. = ( 0g ` R )   &    |- K = { y e. G | ( y |` A ) = ( A X. { .0. } ) }   &    |- F = ( x e. K |-> ( x |` B ) )   &    |- C = ( R ^s A )   &    |- D = ( R ^s B )   &    |- L = ( E ↾s K )   =>    |- ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F e. ( L LMIso D ) )
Theorem	filnm 37660	Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- B = ( Base ` W )   =>    |- ( ( W e. LMod /\ B e. Fin ) -> W e. LNoeM )
Theorem	pwslnmlem0 37661	Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s (/) )   =>    |- ( W e. LMod -> Y e. LNoeM )
Theorem	pwslnmlem1 37662*	First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s { i } )   =>    |- ( W e. LNoeM -> Y e. LNoeM )
Theorem	pwslnmlem2 37663	A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- A e. _V   &    |- B e. _V   &    |- X = ( W ^s A )   &    |- Y = ( W ^s B )   &    |- Z = ( W ^s ( A u. B ) )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> X e. LNoeM )   &    |- ( ph -> Y e. LNoeM )   =>    |- ( ph -> Z e. LNoeM )
Theorem	pwslnm 37664	Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( W ^s I )   =>    |- ( ( W e. LNoeM /\ I e. Fin ) -> Y e. LNoeM )
20.25.40  Every set admits a group structure iff choice
Theorem	unxpwdom3 37665*	Weaker version of unxpwdom 8494 where a function is required only to be cancellative, not an injection. D and B are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into A, each row must hit an element of B; by column injectivity, each row can be identified in at least one way by the B element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. X )   &    |- ( ( ph /\ a e. C /\ b e. D ) -> ( a .+ b ) e. ( A u. B ) )   &    |- ( ( ( ph /\ a e. C ) /\ ( b e. D /\ c e. D ) ) -> ( ( a .+ b ) = ( a .+ c ) <-> b = c ) )   &    |- ( ( ( ph /\ d e. D ) /\ ( a e. C /\ c e. C ) ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )   &    |- ( ph -> -. D ~<_ A )   =>    |- ( ph -> C ~<_* ( D X. B ) )
Theorem	pwfi2f1o 37666*	The pw2f1o 8065 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
|- S = { y e. ( 2o ^m A ) | y finSupp (/) }   &    |- F = ( x e. S |-> ( `' x " { 1o } ) )   =>    |- ( A e. V -> F : S -1-1-onto-> ( ~P A i^i Fin ) )
Theorem	pwfi2en 37667*	Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
|- S = { y e. ( 2o ^m A ) | y finSupp (/) }   =>    |- ( A e. V -> S ~~ ( ~P A i^i Fin ) )
Theorem	frlmpwfi 37668	Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.)
|- R = (ℤ/nℤ ` 2 )   &    |- Y = ( R freeLMod I )   &    |- B = ( Base ` Y )   =>    |- ( I e. V -> B ~~ ( ~P I i^i Fin ) )
Theorem	gicabl 37669	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- ( G ~=g𝑔 H -> ( G e. Abel <-> H e. Abel ) )
Theorem	imasgim 37670	A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -1-1-onto-> B )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> F e. ( R GrpIso U ) )
Theorem	isnumbasgrplem1 37671	A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- B = ( Base ` R )   =>    |- ( ( R e. Abel /\ C ~~ B ) -> C e. ( Base " Abel ) )
Theorem	harn0 37672	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. V -> (har ` S ) =/= (/) )
Theorem	numinfctb 37673	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( ( S e. dom card /\ -. S e. Fin ) -> om ~<_ S )
Theorem	isnumbasgrplem2 37674	If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( ( S u. (har ` S ) ) e. ( Base " Grp ) -> S e. dom card )
Theorem	isnumbasgrplem3 37675	Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ( S e. dom card /\ S =/= (/) ) -> S e. ( Base " Abel ) )
Theorem	isnumbasabl 37676	A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. dom card <-> ( S u. (har ` S ) ) e. ( Base " Abel ) )
Theorem	isnumbasgrp 37677	A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- ( S e. dom card <-> ( S u. (har ` S ) ) e. ( Base " Grp ) )
Theorem	dfacbasgrp 37678	A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.)
|- (CHOICE <-> ( Base " Grp ) = ( _V \ { (/) } ) )
20.25.41  Noetherian rings and left modules II
Syntax	clnr 37679	Extend class notation with the class of left Noetherian rings.
class LNoeR
Definition	df-lnr 37680	A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- LNoeR = { a e. Ring | (ringLMod ` a ) e. LNoeM }
Theorem	islnr 37681	Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR <-> ( A e. Ring /\ (ringLMod ` A ) e. LNoeM ) )
Theorem	lnrring 37682	Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR -> A e. Ring )
Theorem	lnrlnm 37683	Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. LNoeR -> (ringLMod ` A ) e. LNoeM )
Theorem	islnr2 37684*	Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- B = ( Base ` R )   &    |- U = (LIdeal ` R )   &    |- N = (RSpan ` R )   =>    |- ( R e. LNoeR <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
Theorem	islnr3 37685	Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- B = ( Base ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. LNoeR <-> ( R e. Ring /\ U e. (NoeACS ` B ) ) )
Theorem	lnr2i 37686*	Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- U = (LIdeal ` R )   &    |- N = (RSpan ` R )   =>    |- ( ( R e. LNoeR /\ I e. U ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) )
Theorem	lpirlnr 37687	Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( R e. LPIR -> R e. LNoeR )
Theorem	lnrfrlm 37688	Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.)
|- Y = ( R freeLMod I )   =>    |- ( ( R e. LNoeR /\ I e. Fin ) -> Y e. LNoeM )
Theorem	lnrfg 37689	Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015.)
|- S = (Scalar ` M )   =>    |- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )
Theorem	lnrfgtr 37690	A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015.)
|- S = (Scalar ` M )   &    |- U = ( LSubSp ` M )   &    |- N = ( M ↾s P )   =>    |- ( ( M e. LFinGen /\ S e. LNoeR /\ P e. U ) -> N e. LFinGen )
20.25.42  Hilbert's Basis Theorem
Syntax	cldgis 37691	The leading ideal sequence used in the Hilbert Basis Theorem.
class ldgIdlSeq
Definition	df-ldgis 37692*	Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- x elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 37700. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ldgIdlSeq = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) ) )
Theorem	hbtlem1 37693*	Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- D = ( deg1 ` R )   =>    |- ( ( R e. V /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { j | E. k e. I ( ( D ` k ) <_ X /\ j = ( (coe1 ` k ) ` X ) ) } )
Theorem	hbtlem2 37694	Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- T = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) e. T )
Theorem	hbtlem7 37695	Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- T = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> ( S ` I ) : NN0 --> T )
Theorem	hbtlem4 37696	The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> X e. NN0 )   &    |- ( ph -> Y e. NN0 )   &    |- ( ph -> X <_ Y )   =>    |- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` I ) ` Y ) )
Theorem	hbtlem3 37697	The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> J e. U )   &    |- ( ph -> I C_ J )   &    |- ( ph -> X e. NN0 )   =>    |- ( ph -> ( ( S ` I ) ` X ) C_ ( ( S ` J ) ` X ) )
Theorem	hbtlem5 37698*	The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. U )   &    |- ( ph -> J e. U )   &    |- ( ph -> I C_ J )   &    |- ( ph -> A. x e. NN0 ( ( S ` J ) ` x ) C_ ( ( S ` I ) ` x ) )   =>    |- ( ph -> I = J )
Theorem	hbtlem6 37699*	There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- P = (Poly1 ` R )   &    |- U = (LIdeal ` P )   &    |- S = (ldgIdlSeq ` R )   &    |- N = (RSpan ` P )   &    |- ( ph -> R e. LNoeR )   &    |- ( ph -> I e. U )   &    |- ( ph -> X e. NN0 )   =>    |- ( ph -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) )
Theorem	hbt 37700	The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- P = (Poly1 ` R )   =>    |- ( R e. LNoeR -> P e. LNoeR )