Metamath Proof Explorer

Theorem fin23lem29

Description: Lemma for fin23 . The residual is built from the same elements as the previous sequence. (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 fin23lem29 
|- 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 eqif 
 |-  ( Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) <-> ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) )
8 7 biimpi 
 |-  ( Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) -> ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) )
9 rneq 
 |-  ( Z = ( t o. R ) -> ran Z = ran ( t o. R ) )
10 9 unieqd 
 |-  ( Z = ( t o. R ) -> U. ran Z = U. ran ( t o. R ) )
11 rncoss 
 |-  ran ( t o. R ) C_ ran t
12 11 unissi 
 |-  U. ran ( t o. R ) C_ U. ran t
13 10 12 eqsstrdi 
 |-  ( Z = ( t o. R ) -> U. ran Z C_ U. ran t )
14 13 adantl 
 |-  ( ( P e. Fin /\ Z = ( t o. R ) ) -> U. ran Z C_ U. ran t )
15 rneq 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> ran Z = ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
16 15 unieqd 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> U. ran Z = U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) )
17 rncoss 
 |-  ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
18 17 unissi 
 |-  U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
19 unissb 
 |-  ( U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) C_ U. ran t <-> A. a e. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) a C_ U. ran t )
20 abid 
 |-  ( a e. { a | E. z e. P a = ( ( t ` z ) \ |^| ran U ) } <-> E. z e. P a = ( ( t ` z ) \ |^| ran U ) )
21 fvssunirn 
 |-  ( t ` z ) C_ U. ran t
22 21 a1i 
 |-  ( z e. P -> ( t ` z ) C_ U. ran t )
23 22 ssdifssd 
 |-  ( z e. P -> ( ( t ` z ) \ |^| ran U ) C_ U. ran t )
24 sseq1 
 |-  ( a = ( ( t ` z ) \ |^| ran U ) -> ( a C_ U. ran t <-> ( ( t ` z ) \ |^| ran U ) C_ U. ran t ) )
25 23 24 syl5ibrcom 
 |-  ( z e. P -> ( a = ( ( t ` z ) \ |^| ran U ) -> a C_ U. ran t ) )
26 25 rexlimiv 
 |-  ( E. z e. P a = ( ( t ` z ) \ |^| ran U ) -> a C_ U. ran t )
27 20 26 sylbi 
 |-  ( a e. { a | E. z e. P a = ( ( t ` z ) \ |^| ran U ) } -> a C_ U. ran t )
28 eqid 
 |-  ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) = ( z e. P |-> ( ( t ` z ) \ |^| ran U ) )
29 28 rnmpt 
 |-  ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) = { a | E. z e. P a = ( ( t ` z ) \ |^| ran U ) }
30 27 29 eleq2s 
 |-  ( a e. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) -> a C_ U. ran t )
31 19 30 mprgbir 
 |-  U. ran ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) C_ U. ran t
32 18 31 sstri 
 |-  U. ran ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) C_ U. ran t
33 16 32 eqsstrdi 
 |-  ( Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) -> U. ran Z C_ U. ran t )
34 33 adantl 
 |-  ( ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) -> U. ran Z C_ U. ran t )
35 14 34 jaoi 
 |-  ( ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P |-> ( ( t ` z ) \ |^| ran U ) ) o. Q ) ) ) -> U. ran Z C_ U. ran t )
36 6 8 35 mp2b 
 |-  U. ran Z C_ U. ran t