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

Metamath Proof Explorer

Theorem fin23lem29

Proof