This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( 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 bitrid 
 |-  ( 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 ) ) )