Metamath Proof Explorer

Theorem isfin3-3

Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014)

		Ref	Expression
	Assertion	isfin3-3	\|- ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> \|^\| ran f e. ran f ) ) )

Proof

Step	Hyp	Ref	Expression
1		isf33lem	\|- Fin3 = { g \| A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> \|^\| ran a e. ran a ) }
2	1	isfin3ds	\|- ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> \|^\| ran f e. ran f ) ) )

Step

Hyp

Ref

Expression

isf33lem

 |-  Fin3 = { g | A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) }

isfin3ds

 |-  ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )