Metamath Proof Explorer

Theorem fin23lem41

Description: Lemma for fin23 . A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem40.f 
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
Assertion fin23lem41 
|- ( A e. F -> A e. Fin3 )

Proof

Step Hyp Ref Expression
1 fin23lem40.f 
 |-  F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
2 brdomi 
 |-  ( _om ~<_ ~P A -> E. b b : _om -1-1-> ~P A )
3 1 fin23lem33 
 |-  ( A e. F -> E. c A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) )
4 3 adantl 
 |-  ( ( b : _om -1-1-> ~P A /\ A e. F ) -> E. c A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) )
5 ssv 
 |-  ~P A C_ _V
6 f1ss 
 |-  ( ( b : _om -1-1-> ~P A /\ ~P A C_ _V ) -> b : _om -1-1-> _V )
7 5 6 mpan2 
 |-  ( b : _om -1-1-> ~P A -> b : _om -1-1-> _V )
8 7 ad2antrr 
 |-  ( ( ( b : _om -1-1-> ~P A /\ A e. F ) /\ A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) ) -> b : _om -1-1-> _V )
9 f1f 
 |-  ( b : _om -1-1-> ~P A -> b : _om --> ~P A )
10 frn 
 |-  ( b : _om --> ~P A -> ran b C_ ~P A )
11 uniss 
 |-  ( ran b C_ ~P A -> U. ran b C_ U. ~P A )
12 9 10 11 3syl 
 |-  ( b : _om -1-1-> ~P A -> U. ran b C_ U. ~P A )
13 unipw 
 |-  U. ~P A = A
14 12 13 sseqtrdi 
 |-  ( b : _om -1-1-> ~P A -> U. ran b C_ A )
15 14 ad2antrr 
 |-  ( ( ( b : _om -1-1-> ~P A /\ A e. F ) /\ A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) ) -> U. ran b C_ A )
16 f1eq1 
 |-  ( d = e -> ( d : _om -1-1-> _V <-> e : _om -1-1-> _V ) )
17 rneq 
 |-  ( d = e -> ran d = ran e )
18 17 unieqd 
 |-  ( d = e -> U. ran d = U. ran e )
19 18 sseq1d 
 |-  ( d = e -> ( U. ran d C_ A <-> U. ran e C_ A ) )
20 16 19 anbi12d 
 |-  ( d = e -> ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) <-> ( e : _om -1-1-> _V /\ U. ran e C_ A ) ) )
21 fveq2 
 |-  ( d = e -> ( c ` d ) = ( c ` e ) )
22 f1eq1 
 |-  ( ( c ` d ) = ( c ` e ) -> ( ( c ` d ) : _om -1-1-> _V <-> ( c ` e ) : _om -1-1-> _V ) )
23 21 22 syl 
 |-  ( d = e -> ( ( c ` d ) : _om -1-1-> _V <-> ( c ` e ) : _om -1-1-> _V ) )
24 21 rneqd 
 |-  ( d = e -> ran ( c ` d ) = ran ( c ` e ) )
25 24 unieqd 
 |-  ( d = e -> U. ran ( c ` d ) = U. ran ( c ` e ) )
26 25 18 psseq12d 
 |-  ( d = e -> ( U. ran ( c ` d ) C. U. ran d <-> U. ran ( c ` e ) C. U. ran e ) )
27 23 26 anbi12d 
 |-  ( d = e -> ( ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) <-> ( ( c ` e ) : _om -1-1-> _V /\ U. ran ( c ` e ) C. U. ran e ) ) )
28 20 27 imbi12d 
 |-  ( d = e -> ( ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) <-> ( ( e : _om -1-1-> _V /\ U. ran e C_ A ) -> ( ( c ` e ) : _om -1-1-> _V /\ U. ran ( c ` e ) C. U. ran e ) ) ) )
29 28 cbvalvw 
 |-  ( A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) <-> A. e ( ( e : _om -1-1-> _V /\ U. ran e C_ A ) -> ( ( c ` e ) : _om -1-1-> _V /\ U. ran ( c ` e ) C. U. ran e ) ) )
30 29 biimpi 
 |-  ( A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) -> A. e ( ( e : _om -1-1-> _V /\ U. ran e C_ A ) -> ( ( c ` e ) : _om -1-1-> _V /\ U. ran ( c ` e ) C. U. ran e ) ) )
31 30 adantl 
 |-  ( ( ( b : _om -1-1-> ~P A /\ A e. F ) /\ A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) ) -> A. e ( ( e : _om -1-1-> _V /\ U. ran e C_ A ) -> ( ( c ` e ) : _om -1-1-> _V /\ U. ran ( c ` e ) C. U. ran e ) ) )
32 eqid 
 |-  ( rec ( c , b ) |` _om ) = ( rec ( c , b ) |` _om )
33 1 8 15 31 32 fin23lem39 
 |-  ( ( ( b : _om -1-1-> ~P A /\ A e. F ) /\ A. d ( ( d : _om -1-1-> _V /\ U. ran d C_ A ) -> ( ( c ` d ) : _om -1-1-> _V /\ U. ran ( c ` d ) C. U. ran d ) ) ) -> -. A e. F )
34 4 33 exlimddv 
 |-  ( ( b : _om -1-1-> ~P A /\ A e. F ) -> -. A e. F )
35 34 pm2.01da 
 |-  ( b : _om -1-1-> ~P A -> -. A e. F )
36 35 exlimiv 
 |-  ( E. b b : _om -1-1-> ~P A -> -. A e. F )
37 2 36 syl 
 |-  ( _om ~<_ ~P A -> -. A e. F )
38 37 con2i 
 |-  ( A e. F -> -. _om ~<_ ~P A )
39 pwexg 
 |-  ( A e. F -> ~P A e. _V )
40 isfin4-2 
 |-  ( ~P A e. _V -> ( ~P A e. Fin4 <-> -. _om ~<_ ~P A ) )
41 39 40 syl 
 |-  ( A e. F -> ( ~P A e. Fin4 <-> -. _om ~<_ ~P A ) )
42 38 41 mpbird 
 |-  ( A e. F -> ~P A e. Fin4 )
43 isfin3 
 |-  ( A e. Fin3 <-> ~P A e. Fin4 )
44 42 43 sylibr 
 |-  ( A e. F -> A e. Fin3 )