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 fex 
 |-  ( ( Z : _om --> _V /\ _om e. _V ) -> Z e. _V )
34 32 28 33 syl2anc 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> Z e. _V )
35 eqid 
 |-  ( t e. ( ~P G ^m _om ) |-> Z ) = ( t e. ( ~P G ^m _om ) |-> Z )
36 35 fvmpt2 
 |-  ( ( t e. ( ~P G ^m _om ) /\ Z e. _V ) -> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z )
37 30 34 36 syl2anc 
 |-  ( ( G e. F /\ ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) -> ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z )
38 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 ) )
39 rneq 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = ran Z )
40 39 unieqd 
 |-  ( ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = Z -> U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) = U. ran Z )
41 40 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 ) )
42 38 41 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 ) ) )
43 37 42 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 ) ) )
44 8 13 43 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 ) )
45 44 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 ) ) )
46 45 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 ) ) )
47 ovex 
 |-  ( ~P G ^m _om ) e. _V
48 47 mptex 
 |-  ( t e. ( ~P G ^m _om ) |-> Z ) e. _V
49 nfmpt1 
 |-  F/_ t ( t e. ( ~P G ^m _om ) |-> Z )
50 49 nfeq2 
 |-  F/ t f = ( t e. ( ~P G ^m _om ) |-> Z )
51 fveq1 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ( f ` t ) = ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
52 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 ) )
53 51 52 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 ) )
54 51 rneqd 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> ran ( f ` t ) = ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
55 54 unieqd 
 |-  ( f = ( t e. ( ~P G ^m _om ) |-> Z ) -> U. ran ( f ` t ) = U. ran ( ( t e. ( ~P G ^m _om ) |-> Z ) ` t ) )
56 55 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 ) )
57 53 56 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 ) ) )
58 57 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 ) ) ) )
59 50 58 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 ) ) ) )
60 48 59 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 ) ) )
61 46 60 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 ) ) )
62 f1eq1 
 |-  ( b = t -> ( b : _om -1-1-> _V <-> t : _om -1-1-> _V ) )
63 rneq 
 |-  ( b = t -> ran b = ran t )
64 63 unieqd 
 |-  ( b = t -> U. ran b = U. ran t )
65 64 sseq1d 
 |-  ( b = t -> ( U. ran b C_ G <-> U. ran t C_ G ) )
66 62 65 anbi12d 
 |-  ( b = t -> ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) <-> ( t : _om -1-1-> _V /\ U. ran t C_ G ) ) )
67 fveq2 
 |-  ( b = t -> ( f ` b ) = ( f ` t ) )
68 f1eq1 
 |-  ( ( f ` b ) = ( f ` t ) -> ( ( f ` b ) : _om -1-1-> _V <-> ( f ` t ) : _om -1-1-> _V ) )
69 67 68 syl 
 |-  ( b = t -> ( ( f ` b ) : _om -1-1-> _V <-> ( f ` t ) : _om -1-1-> _V ) )
70 67 rneqd 
 |-  ( b = t -> ran ( f ` b ) = ran ( f ` t ) )
71 70 unieqd 
 |-  ( b = t -> U. ran ( f ` b ) = U. ran ( f ` t ) )
72 71 64 psseq12d 
 |-  ( b = t -> ( U. ran ( f ` b ) C. U. ran b <-> U. ran ( f ` t ) C. U. ran t ) )
73 69 72 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 ) ) )
74 66 73 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 ) ) ) )
75 74 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 ) ) )
76 75 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 ) ) )
77 61 76 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 ) ) )