Metamath Proof Explorer

Theorem isf34lem6

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a 
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem6 
|- ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) ) )

Proof

Step Hyp Ref Expression
1 compss.a 
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 elmapi 
 |-  ( f e. ( ~P A ^m _om ) -> f : _om --> ~P A )
3 1 isf34lem7 
 |-  ( ( A e. Fin3 /\ f : _om --> ~P A /\ A. y e. _om ( f ` y ) C_ ( f ` suc y ) ) -> U. ran f e. ran f )
4 3 3expia 
 |-  ( ( A e. Fin3 /\ f : _om --> ~P A ) -> ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) )
5 2 4 sylan2 
 |-  ( ( A e. Fin3 /\ f e. ( ~P A ^m _om ) ) -> ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) )
6 5 ralrimiva 
 |-  ( A e. Fin3 -> A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) )
7 elmapex 
 |-  ( g e. ( ~P A ^m _om ) -> ( ~P A e. _V /\ _om e. _V ) )
8 7 simpld 
 |-  ( g e. ( ~P A ^m _om ) -> ~P A e. _V )
9 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
10 8 9 sylibr 
 |-  ( g e. ( ~P A ^m _om ) -> A e. _V )
11 1 isf34lem2 
 |-  ( A e. _V -> F : ~P A --> ~P A )
12 10 11 syl 
 |-  ( g e. ( ~P A ^m _om ) -> F : ~P A --> ~P A )
13 elmapi 
 |-  ( g e. ( ~P A ^m _om ) -> g : _om --> ~P A )
14 fco 
 |-  ( ( F : ~P A --> ~P A /\ g : _om --> ~P A ) -> ( F o. g ) : _om --> ~P A )
15 12 13 14 syl2anc 
 |-  ( g e. ( ~P A ^m _om ) -> ( F o. g ) : _om --> ~P A )
16 elmapg 
 |-  ( ( ~P A e. _V /\ _om e. _V ) -> ( ( F o. g ) e. ( ~P A ^m _om ) <-> ( F o. g ) : _om --> ~P A ) )
17 7 16 syl 
 |-  ( g e. ( ~P A ^m _om ) -> ( ( F o. g ) e. ( ~P A ^m _om ) <-> ( F o. g ) : _om --> ~P A ) )
18 15 17 mpbird 
 |-  ( g e. ( ~P A ^m _om ) -> ( F o. g ) e. ( ~P A ^m _om ) )
19 fveq1 
 |-  ( f = ( F o. g ) -> ( f ` y ) = ( ( F o. g ) ` y ) )
20 fveq1 
 |-  ( f = ( F o. g ) -> ( f ` suc y ) = ( ( F o. g ) ` suc y ) )
21 19 20 sseq12d 
 |-  ( f = ( F o. g ) -> ( ( f ` y ) C_ ( f ` suc y ) <-> ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) ) )
22 21 ralbidv 
 |-  ( f = ( F o. g ) -> ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) <-> A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) ) )
23 rneq 
 |-  ( f = ( F o. g ) -> ran f = ran ( F o. g ) )
24 rnco2 
 |-  ran ( F o. g ) = ( F " ran g )
25 23 24 eqtrdi 
 |-  ( f = ( F o. g ) -> ran f = ( F " ran g ) )
26 25 unieqd 
 |-  ( f = ( F o. g ) -> U. ran f = U. ( F " ran g ) )
27 26 25 eleq12d 
 |-  ( f = ( F o. g ) -> ( U. ran f e. ran f <-> U. ( F " ran g ) e. ( F " ran g ) ) )
28 22 27 imbi12d 
 |-  ( f = ( F o. g ) -> ( ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) <-> ( A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) -> U. ( F " ran g ) e. ( F " ran g ) ) ) )
29 28 rspccv 
 |-  ( A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) -> ( ( F o. g ) e. ( ~P A ^m _om ) -> ( A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) -> U. ( F " ran g ) e. ( F " ran g ) ) ) )
30 18 29 syl5 
 |-  ( A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) -> ( g e. ( ~P A ^m _om ) -> ( A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) -> U. ( F " ran g ) e. ( F " ran g ) ) ) )
31 sscon 
 |-  ( ( g ` suc y ) C_ ( g ` y ) -> ( A \ ( g ` y ) ) C_ ( A \ ( g ` suc y ) ) )
32 13 ffvelcdmda 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( g ` y ) e. ~P A )
33 32 elpwid 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( g ` y ) C_ A )
34 1 isf34lem1 
 |-  ( ( A e. _V /\ ( g ` y ) C_ A ) -> ( F ` ( g ` y ) ) = ( A \ ( g ` y ) ) )
35 10 33 34 syl2an2r 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( F ` ( g ` y ) ) = ( A \ ( g ` y ) ) )
36 peano2 
 |-  ( y e. _om -> suc y e. _om )
37 ffvelcdm 
 |-  ( ( g : _om --> ~P A /\ suc y e. _om ) -> ( g ` suc y ) e. ~P A )
38 13 36 37 syl2an 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( g ` suc y ) e. ~P A )
39 38 elpwid 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( g ` suc y ) C_ A )
40 1 isf34lem1 
 |-  ( ( A e. _V /\ ( g ` suc y ) C_ A ) -> ( F ` ( g ` suc y ) ) = ( A \ ( g ` suc y ) ) )
41 10 39 40 syl2an2r 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( F ` ( g ` suc y ) ) = ( A \ ( g ` suc y ) ) )
42 35 41 sseq12d 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( F ` ( g ` y ) ) C_ ( F ` ( g ` suc y ) ) <-> ( A \ ( g ` y ) ) C_ ( A \ ( g ` suc y ) ) ) )
43 31 42 imbitrrid 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( g ` suc y ) C_ ( g ` y ) -> ( F ` ( g ` y ) ) C_ ( F ` ( g ` suc y ) ) ) )
44 fvco3 
 |-  ( ( g : _om --> ~P A /\ y e. _om ) -> ( ( F o. g ) ` y ) = ( F ` ( g ` y ) ) )
45 13 44 sylan 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( F o. g ) ` y ) = ( F ` ( g ` y ) ) )
46 fvco3 
 |-  ( ( g : _om --> ~P A /\ suc y e. _om ) -> ( ( F o. g ) ` suc y ) = ( F ` ( g ` suc y ) ) )
47 13 36 46 syl2an 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( F o. g ) ` suc y ) = ( F ` ( g ` suc y ) ) )
48 45 47 sseq12d 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) <-> ( F ` ( g ` y ) ) C_ ( F ` ( g ` suc y ) ) ) )
49 43 48 sylibrd 
 |-  ( ( g e. ( ~P A ^m _om ) /\ y e. _om ) -> ( ( g ` suc y ) C_ ( g ` y ) -> ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) ) )
50 49 ralimdva 
 |-  ( g e. ( ~P A ^m _om ) -> ( A. y e. _om ( g ` suc y ) C_ ( g ` y ) -> A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) ) )
51 12 ffnd 
 |-  ( g e. ( ~P A ^m _om ) -> F Fn ~P A )
52 imassrn 
 |-  ( F " ran g ) C_ ran F
53 12 frnd 
 |-  ( g e. ( ~P A ^m _om ) -> ran F C_ ~P A )
54 52 53 sstrid 
 |-  ( g e. ( ~P A ^m _om ) -> ( F " ran g ) C_ ~P A )
55 fnfvima 
 |-  ( ( F Fn ~P A /\ ( F " ran g ) C_ ~P A /\ U. ( F " ran g ) e. ( F " ran g ) ) -> ( F ` U. ( F " ran g ) ) e. ( F " ( F " ran g ) ) )
56 55 3expia 
 |-  ( ( F Fn ~P A /\ ( F " ran g ) C_ ~P A ) -> ( U. ( F " ran g ) e. ( F " ran g ) -> ( F ` U. ( F " ran g ) ) e. ( F " ( F " ran g ) ) ) )
57 51 54 56 syl2anc 
 |-  ( g e. ( ~P A ^m _om ) -> ( U. ( F " ran g ) e. ( F " ran g ) -> ( F ` U. ( F " ran g ) ) e. ( F " ( F " ran g ) ) ) )
58 incom 
 |-  ( dom F i^i ran g ) = ( ran g i^i dom F )
59 13 frnd 
 |-  ( g e. ( ~P A ^m _om ) -> ran g C_ ~P A )
60 12 fdmd 
 |-  ( g e. ( ~P A ^m _om ) -> dom F = ~P A )
61 59 60 sseqtrrd 
 |-  ( g e. ( ~P A ^m _om ) -> ran g C_ dom F )
62 dfss2 
 |-  ( ran g C_ dom F <-> ( ran g i^i dom F ) = ran g )
63 61 62 sylib 
 |-  ( g e. ( ~P A ^m _om ) -> ( ran g i^i dom F ) = ran g )
64 58 63 eqtrid 
 |-  ( g e. ( ~P A ^m _om ) -> ( dom F i^i ran g ) = ran g )
65 13 fdmd 
 |-  ( g e. ( ~P A ^m _om ) -> dom g = _om )
66 peano1 
 |-  (/) e. _om
67 ne0i 
 |-  ( (/) e. _om -> _om =/= (/) )
68 66 67 mp1i 
 |-  ( g e. ( ~P A ^m _om ) -> _om =/= (/) )
69 65 68 eqnetrd 
 |-  ( g e. ( ~P A ^m _om ) -> dom g =/= (/) )
70 dm0rn0 
 |-  ( dom g = (/) <-> ran g = (/) )
71 70 necon3bii 
 |-  ( dom g =/= (/) <-> ran g =/= (/) )
72 69 71 sylib 
 |-  ( g e. ( ~P A ^m _om ) -> ran g =/= (/) )
73 64 72 eqnetrd 
 |-  ( g e. ( ~P A ^m _om ) -> ( dom F i^i ran g ) =/= (/) )
74 imadisj 
 |-  ( ( F " ran g ) = (/) <-> ( dom F i^i ran g ) = (/) )
75 74 necon3bii 
 |-  ( ( F " ran g ) =/= (/) <-> ( dom F i^i ran g ) =/= (/) )
76 73 75 sylibr 
 |-  ( g e. ( ~P A ^m _om ) -> ( F " ran g ) =/= (/) )
77 1 isf34lem4 
 |-  ( ( A e. _V /\ ( ( F " ran g ) C_ ~P A /\ ( F " ran g ) =/= (/) ) ) -> ( F ` U. ( F " ran g ) ) = |^| ( F " ( F " ran g ) ) )
78 10 54 76 77 syl12anc 
 |-  ( g e. ( ~P A ^m _om ) -> ( F ` U. ( F " ran g ) ) = |^| ( F " ( F " ran g ) ) )
79 1 isf34lem3 
 |-  ( ( A e. _V /\ ran g C_ ~P A ) -> ( F " ( F " ran g ) ) = ran g )
80 10 59 79 syl2anc 
 |-  ( g e. ( ~P A ^m _om ) -> ( F " ( F " ran g ) ) = ran g )
81 80 inteqd 
 |-  ( g e. ( ~P A ^m _om ) -> |^| ( F " ( F " ran g ) ) = |^| ran g )
82 78 81 eqtrd 
 |-  ( g e. ( ~P A ^m _om ) -> ( F ` U. ( F " ran g ) ) = |^| ran g )
83 82 80 eleq12d 
 |-  ( g e. ( ~P A ^m _om ) -> ( ( F ` U. ( F " ran g ) ) e. ( F " ( F " ran g ) ) <-> |^| ran g e. ran g ) )
84 57 83 sylibd 
 |-  ( g e. ( ~P A ^m _om ) -> ( U. ( F " ran g ) e. ( F " ran g ) -> |^| ran g e. ran g ) )
85 50 84 imim12d 
 |-  ( g e. ( ~P A ^m _om ) -> ( ( A. y e. _om ( ( F o. g ) ` y ) C_ ( ( F o. g ) ` suc y ) -> U. ( F " ran g ) e. ( F " ran g ) ) -> ( A. y e. _om ( g ` suc y ) C_ ( g ` y ) -> |^| ran g e. ran g ) ) )
86 30 85 sylcom 
 |-  ( A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) -> ( g e. ( ~P A ^m _om ) -> ( A. y e. _om ( g ` suc y ) C_ ( g ` y ) -> |^| ran g e. ran g ) ) )
87 86 ralrimiv 
 |-  ( A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) -> A. g e. ( ~P A ^m _om ) ( A. y e. _om ( g ` suc y ) C_ ( g ` y ) -> |^| ran g e. ran g ) )
88 isfin3-3 
 |-  ( A e. V -> ( A e. Fin3 <-> A. g e. ( ~P A ^m _om ) ( A. y e. _om ( g ` suc y ) C_ ( g ` y ) -> |^| ran g e. ran g ) ) )
89 87 88 imbitrrid 
 |-  ( A e. V -> ( A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) -> A e. Fin3 ) )
90 6 89 impbid2 
 |-  ( A e. V -> ( A e. Fin3 <-> A. f e. ( ~P A ^m _om ) ( A. y e. _om ( f ` y ) C_ ( f ` suc y ) -> U. ran f e. ran f ) ) )