Metamath Proof Explorer


Theorem isfin3ds

Description: Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Hypothesis isfin3ds.f
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) }
Assertion isfin3ds
|- ( A e. V -> ( A e. F <-> 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 isfin3ds.f
 |-  F = { g | A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) }
2 suceq
 |-  ( b = x -> suc b = suc x )
3 2 fveq2d
 |-  ( b = x -> ( a ` suc b ) = ( a ` suc x ) )
4 fveq2
 |-  ( b = x -> ( a ` b ) = ( a ` x ) )
5 3 4 sseq12d
 |-  ( b = x -> ( ( a ` suc b ) C_ ( a ` b ) <-> ( a ` suc x ) C_ ( a ` x ) ) )
6 5 cbvralvw
 |-  ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) <-> A. x e. _om ( a ` suc x ) C_ ( a ` x ) )
7 fveq1
 |-  ( a = f -> ( a ` suc x ) = ( f ` suc x ) )
8 fveq1
 |-  ( a = f -> ( a ` x ) = ( f ` x ) )
9 7 8 sseq12d
 |-  ( a = f -> ( ( a ` suc x ) C_ ( a ` x ) <-> ( f ` suc x ) C_ ( f ` x ) ) )
10 9 ralbidv
 |-  ( a = f -> ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) <-> A. x e. _om ( f ` suc x ) C_ ( f ` x ) ) )
11 6 10 syl5bb
 |-  ( a = f -> ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) <-> A. x e. _om ( f ` suc x ) C_ ( f ` x ) ) )
12 rneq
 |-  ( a = f -> ran a = ran f )
13 12 inteqd
 |-  ( a = f -> |^| ran a = |^| ran f )
14 13 12 eleq12d
 |-  ( a = f -> ( |^| ran a e. ran a <-> |^| ran f e. ran f ) )
15 11 14 imbi12d
 |-  ( a = f -> ( ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )
16 15 cbvralvw
 |-  ( A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> A. f e. ( ~P g ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) )
17 pweq
 |-  ( g = A -> ~P g = ~P A )
18 17 oveq1d
 |-  ( g = A -> ( ~P g ^m _om ) = ( ~P A ^m _om ) )
19 18 raleqdv
 |-  ( g = A -> ( A. f e. ( ~P g ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )
20 16 19 syl5bb
 |-  ( g = A -> ( A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )
21 20 1 elab2g
 |-  ( A e. V -> ( A e. F <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) )