Metamath Proof Explorer

Theorem fin23lem17

Description: Lemma for fin23 . By ? Fin3DS ? , U achieves its minimum ( X in the synopsis above, but we will not be assigning a symbol here). TODO: Fix comment; math symbol Fin3DS does not exist. (Contributed by Stefan O'Rear, 4-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

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 ) }
Assertion fin23lem17 
|- ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U e. ran U )

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 1 fin23lem13 
 |-  ( c e. _om -> ( U ` suc c ) C_ ( U ` c ) )
4 3 rgen 
 |-  A. c e. _om ( U ` suc c ) C_ ( U ` c )
5 fveq1 
 |-  ( b = U -> ( b ` suc c ) = ( U ` suc c ) )
6 fveq1 
 |-  ( b = U -> ( b ` c ) = ( U ` c ) )
7 5 6 sseq12d 
 |-  ( b = U -> ( ( b ` suc c ) C_ ( b ` c ) <-> ( U ` suc c ) C_ ( U ` c ) ) )
8 7 ralbidv 
 |-  ( b = U -> ( A. c e. _om ( b ` suc c ) C_ ( b ` c ) <-> A. c e. _om ( U ` suc c ) C_ ( U ` c ) ) )
9 rneq 
 |-  ( b = U -> ran b = ran U )
10 9 inteqd 
 |-  ( b = U -> |^| ran b = |^| ran U )
11 10 9 eleq12d 
 |-  ( b = U -> ( |^| ran b e. ran b <-> |^| ran U e. ran U ) )
12 8 11 imbi12d 
 |-  ( b = U -> ( ( A. c e. _om ( b ` suc c ) C_ ( b ` c ) -> |^| ran b e. ran b ) <-> ( A. c e. _om ( U ` suc c ) C_ ( U ` c ) -> |^| ran U e. ran U ) ) )
13 2 isfin3ds 
 |-  ( U. ran t e. F -> ( U. ran t e. F <-> A. b e. ( ~P U. ran t ^m _om ) ( A. c e. _om ( b ` suc c ) C_ ( b ` c ) -> |^| ran b e. ran b ) ) )
14 13 ibi 
 |-  ( U. ran t e. F -> A. b e. ( ~P U. ran t ^m _om ) ( A. c e. _om ( b ` suc c ) C_ ( b ` c ) -> |^| ran b e. ran b ) )
15 14 adantr 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> A. b e. ( ~P U. ran t ^m _om ) ( A. c e. _om ( b ` suc c ) C_ ( b ` c ) -> |^| ran b e. ran b ) )
16 1 fnseqom 
 |-  U Fn _om
17 dffn3 
 |-  ( U Fn _om <-> U : _om --> ran U )
18 16 17 mpbi 
 |-  U : _om --> ran U
19 pwuni 
 |-  ran U C_ ~P U. ran U
20 1 fin23lem16 
 |-  U. ran U = U. ran t
21 20 pweqi 
 |-  ~P U. ran U = ~P U. ran t
22 19 21 sseqtri 
 |-  ran U C_ ~P U. ran t
23 fss 
 |-  ( ( U : _om --> ran U /\ ran U C_ ~P U. ran t ) -> U : _om --> ~P U. ran t )
24 18 22 23 mp2an 
 |-  U : _om --> ~P U. ran t
25 vex 
 |-  t e. _V
26 25 rnex 
 |-  ran t e. _V
27 26 uniex 
 |-  U. ran t e. _V
28 27 pwex 
 |-  ~P U. ran t e. _V
29 f1f 
 |-  ( t : _om -1-1-> V -> t : _om --> V )
30 dmfex 
 |-  ( ( t e. _V /\ t : _om --> V ) -> _om e. _V )
31 25 29 30 sylancr 
 |-  ( t : _om -1-1-> V -> _om e. _V )
32 31 adantl 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> _om e. _V )
33 elmapg 
 |-  ( ( ~P U. ran t e. _V /\ _om e. _V ) -> ( U e. ( ~P U. ran t ^m _om ) <-> U : _om --> ~P U. ran t ) )
34 28 32 33 sylancr 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> ( U e. ( ~P U. ran t ^m _om ) <-> U : _om --> ~P U. ran t ) )
35 24 34 mpbiri 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> U e. ( ~P U. ran t ^m _om ) )
36 12 15 35 rspcdva 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> ( A. c e. _om ( U ` suc c ) C_ ( U ` c ) -> |^| ran U e. ran U ) )
37 4 36 mpi 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U e. ran U )