Metamath Proof Explorer

Theorem fin23lem31

Description: Lemma for fin23 . The residual is has a strictly smaller range than the previous sequence. This will be iterated to build an unbounded chain. (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 fin23lem31 
|- ( ( t : _om -1-1-> V /\ G e. F /\ U. ran t C_ G ) -> U. ran Z C. U. ran t )

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 2 ssfin3ds 
 |-  ( ( G e. F /\ U. ran t C_ G ) -> U. ran t e. F )
8 1 2 3 4 5 6 fin23lem29 
 |-  U. ran Z C_ U. ran t
9 8 a1i 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> U. ran Z C_ U. ran t )
10 1 2 fin23lem21 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U =/= (/) )
11 10 ancoms 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> |^| ran U =/= (/) )
12 n0 
 |-  ( |^| ran U =/= (/) <-> E. a a e. |^| ran U )
13 11 12 sylib 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> E. a a e. |^| ran U )
14 1 fnseqom 
 |-  U Fn _om
15 fndm 
 |-  ( U Fn _om -> dom U = _om )
16 14 15 ax-mp 
 |-  dom U = _om
17 peano1 
 |-  (/) e. _om
18 17 ne0ii 
 |-  _om =/= (/)
19 16 18 eqnetri 
 |-  dom U =/= (/)
20 dm0rn0 
 |-  ( dom U = (/) <-> ran U = (/) )
21 20 necon3bii 
 |-  ( dom U =/= (/) <-> ran U =/= (/) )
22 19 21 mpbi 
 |-  ran U =/= (/)
23 intssuni 
 |-  ( ran U =/= (/) -> |^| ran U C_ U. ran U )
24 22 23 ax-mp 
 |-  |^| ran U C_ U. ran U
25 1 fin23lem16 
 |-  U. ran U = U. ran t
26 24 25 sseqtri 
 |-  |^| ran U C_ U. ran t
27 26 sseli 
 |-  ( a e. |^| ran U -> a e. U. ran t )
28 f1fun 
 |-  ( t : _om -1-1-> V -> Fun t )
29 28 adantr 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> Fun t )
30 1 2 3 4 5 6 fin23lem30 
 |-  ( Fun t -> ( U. ran Z i^i |^| ran U ) = (/) )
31 29 30 syl 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> ( U. ran Z i^i |^| ran U ) = (/) )
32 disj 
 |-  ( ( U. ran Z i^i |^| ran U ) = (/) <-> A. a e. U. ran Z -. a e. |^| ran U )
33 31 32 sylib 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> A. a e. U. ran Z -. a e. |^| ran U )
34 rsp 
 |-  ( A. a e. U. ran Z -. a e. |^| ran U -> ( a e. U. ran Z -> -. a e. |^| ran U ) )
35 33 34 syl 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> ( a e. U. ran Z -> -. a e. |^| ran U ) )
36 35 con2d 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> ( a e. |^| ran U -> -. a e. U. ran Z ) )
37 36 imp 
 |-  ( ( ( t : _om -1-1-> V /\ U. ran t e. F ) /\ a e. |^| ran U ) -> -. a e. U. ran Z )
38 nelne1 
 |-  ( ( a e. U. ran t /\ -. a e. U. ran Z ) -> U. ran t =/= U. ran Z )
39 27 37 38 syl2an2 
 |-  ( ( ( t : _om -1-1-> V /\ U. ran t e. F ) /\ a e. |^| ran U ) -> U. ran t =/= U. ran Z )
40 39 necomd 
 |-  ( ( ( t : _om -1-1-> V /\ U. ran t e. F ) /\ a e. |^| ran U ) -> U. ran Z =/= U. ran t )
41 13 40 exlimddv 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> U. ran Z =/= U. ran t )
42 df-pss 
 |-  ( U. ran Z C. U. ran t <-> ( U. ran Z C_ U. ran t /\ U. ran Z =/= U. ran t ) )
43 9 41 42 sylanbrc 
 |-  ( ( t : _om -1-1-> V /\ U. ran t e. F ) -> U. ran Z C. U. ran t )
44 7 43 sylan2 
 |-  ( ( t : _om -1-1-> V /\ ( G e. F /\ U. ran t C_ G ) ) -> U. ran Z C. U. ran t )
45 44 3impb 
 |-  ( ( t : _om -1-1-> V /\ G e. F /\ U. ran t C_ G ) -> U. ran Z C. U. ran t )