Metamath Proof Explorer

Theorem fin23lem32

Description: Lemma for fin23 . Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem.a 
|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
fin23lem17.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 ) }
fin23lem.b 
|- P = { v e. _om | |^| ran U C_ ( t ` v ) }
fin23lem.c 
|- Q = ( w e. _om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
fin23lem.d 
|- R = ( w e. _om |-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
fin23lem.e 
|- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
Assertion fin23lem32 
|- ( G e. F -> E. f A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )

Proof

Step Hyp Ref Expression
1 fin23lem.a 
 |-  U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2 fin23lem17.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 ) }
3 fin23lem.b 
 |-  P = { v e. _om | |^| ran U C_ ( t ` v ) }
4 fin23lem.c 
 |-  Q = ( w e. _om |-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
5 fin23lem.d 
 |-  R = ( w e. _om |-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
6 fin23lem.e 
 |-  Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
7 1 2 3 4 5 6 fin23lem28 
 |-  ( t : _om -1-1-> _V -> Z : _om -1-1-> _V )
8 7 ad2antrl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> Z : _om -1-1-> _V )
9 simprl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> t : _om -1-1-> _V )
10 simpl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> G e. F )
11 simprr 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> U. ran t C_ G )
12 1 2 3 4 5 6 fin23lem31 
 |-  ( ( t : _om -1-1-> _V /\ G e. F /\ U. ran t C_ G ) -> U. ran Z C. U. ran t )
13 9 10 11 12 syl3anc 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> U. ran Z C. U. ran t )
14 f1fn 
 |-  ( t : _om -1-1-> _V -> t Fn _om )
15 dffn3 
 |-  ( t Fn _om <-> t : _om --> ran t )
16 14 15 sylib 
 |-  ( t : _om -1-1-> _V -> t : _om --> ran t )
17 16 ad2antrl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> t : _om --> ran t )
18 sspwuni 
 |-  ( ran t C_ ~P G <-> U. ran t C_ G )
19 18 biimpri 
 |-  ( U. ran t C_ G -> ran t C_ ~P G )
20 19 ad2antll 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ran t C_ ~P G )
21 17 20 fssd 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> t : _om --> ~P G )
22 pwexg 
 |-  ( G e. F -> ~P G e. _V )
23 22 adantr 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ~P G e. _V )
24 vex 
 |-  t e. _V
25 f1f 
 |-  ( t : _om -1-1-> _V -> t : _om --> _V )
26 dmfex 
 |-  ( ( t e. _V /\ t : _om --> _V ) -> _om e. _V )
27 24 25 26 sylancr 
 |-  ( t : _om -1-1-> _V -> _om e. _V )
28 27 ad2antrl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> _om e. _V )
29 23 28 elmapd 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ( t e. ( ~P G ^m _om ) <-> t : _om --> ~P G ) )
30 21 29 mpbird 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> t e. ( ~P G ^m _om ) )
31 f1f 
 |-  ( Z : _om -1-1-> _V -> Z : _om --> _V )
32 8 31 syl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> Z : _om --> _V )
33 32 28 fexd 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> Z e. _V )
34 eqid 
 |-  ( t e. ( ~P G ^m _om ) |-> Z ) = ( t e. ( ~P G ^m _om ) |-> Z )
35 34 fvmpt2 
 |-  ( ( t e. ( ~P G ^m _om ) /\ Z e. _V ) -> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z )
36 30 33 35 syl2anc 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z )
37 f1eq1 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V <-> Z : _om -1-1-> _V ) )
38 rneq 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = ran Z )
39 38 unieqd 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = U. ran Z )
40 39 psseq1d 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> ( U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t <-> U. ran Z C. U. ran t ) )
41 37 40 anbi12d 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> ( ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) <-> ( Z : _om -1-1-> _V /\ U. ran Z C. U. ran t ) ) )
42 36 41 syl 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ( ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) <-> ( Z : _om -1-1-> _V /\ U. ran Z C. U. ran t ) ) )
43 8 13 42 mpbir2and 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) )
44 43 ex 
 |-  ( G e. F -> ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) )
45 44 alrimiv 
 |-  ( G e. F -> A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) )
46 ovex 
 |-  ( ~P G ^m _om ) e. _V
47 46 mptex 
 |-  ( t e. ( ~P G ^m _om ) |-> Z ) e. _V
48 nfmpt1 
 |-  F/_ t ( t e. ( ~P G ^m _om ) |-> Z )
49 48 nfeq2 
 |-  F/ t f = ( t e. ( ~P G ^m _om ) |-> Z )
50 fveq1 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( f ` t ) = ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
51 f1eq1 
 |-  ( ( f ` t ) = ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) -> ( ( f ` t ) : _om -1-1-> _V <-> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V ) )
52 50 51 syl 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( ( f ` t ) : _om -1-1-> _V <-> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V ) )
53 50 rneqd 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ran ( f ` t ) = ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
54 53 unieqd 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> U. ran ( f ` t ) = U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
55 54 psseq1d 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( U. ran ( f ` t ) C. U. ran t <-> U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) )
56 52 55 anbi12d 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) <-> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) )
57 56 imbi2d 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) <-> ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) ) )
58 49 57 albid 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) <-> A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) ) )
59 47 58 spcev 
 |-  ( A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) : _om -1-1-> _V /\ U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) C. U. ran t ) ) -> E. f A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) )
60 45 59 syl 
 |-  ( G e. F -> E. f A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) )
61 f1eq1 
 |-  ( b = t -> ( b : _om -1-1-> _V <-> t : _om -1-1-> _V ) )
62 rneq 
 |-  ( b = t -> ran b = ran t )
63 62 unieqd 
 |-  ( b = t -> U. ran b = U. ran t )
64 63 sseq1d 
 |-  ( b = t -> ( U. ran b C_ G <-> U. ran t C_ G ) )
65 61 64 anbi12d 
 |-  ( b = t -> ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) <-> ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) )
66 fveq2 
 |-  ( b = t -> ( f ` b ) = ( f ` t ) )
67 f1eq1 
 |-  ( ( f ` b ) = ( f ` t ) -> ( ( f ` b ) : _om -1-1-> _V <-> ( f ` t ) : _om -1-1-> _V ) )
68 66 67 syl 
 |-  ( b = t -> ( ( f ` b ) : _om -1-1-> _V <-> ( f ` t ) : _om -1-1-> _V ) )
69 66 rneqd 
 |-  ( b = t -> ran ( f ` b ) = ran ( f ` t ) )
70 69 unieqd 
 |-  ( b = t -> U. ran ( f ` b ) = U. ran ( f ` t ) )
71 70 63 psseq12d 
 |-  ( b = t -> ( U. ran ( f ` b ) C. U. ran b <-> U. ran ( f ` t ) C. U. ran t ) )
72 68 71 anbi12d 
 |-  ( b = t -> ( ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) <-> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) )
73 65 72 imbi12d 
 |-  ( b = t -> ( ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) <-> ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) ) )
74 73 cbvalvw 
 |-  ( A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) <-> A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) )
75 74 exbii 
 |-  ( E. f A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) <-> E. f A. t ( ( t : _om -1-1-> _V /\ U. ran t C_ G ) -> ( ( f ` t ) : _om -1-1-> _V /\ U. ran ( f ` t ) C. U. ran t ) ) )
76 60 75 sylibr 
 |-  ( G e. F -> E. f A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )