isf32lem8

Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014)

	Ref	Expression
Hypotheses	isf32lem.a	\|- ( ph -> F : _om --> ~P G )
	isf32lem.b	\|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
	isf32lem.c	\|- ( ph -> -. \|^\| ran F e. ran F )
	isf32lem.d	\|- S = { y e. _om \| ( F ` suc y ) C. ( F ` y ) }
	isf32lem.e	\|- J = ( u e. _om \|-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
	isf32lem.f	\|- K = ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
Assertion	isf32lem8	\|- ( ( ph /\ A e. _om ) -> ( K ` A ) C_ G )

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	\|- ( ph -> F : _om --> ~P G )
2		isf32lem.b	\|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3		isf32lem.c	\|- ( ph -> -. \|^\| ran F e. ran F )
4		isf32lem.d	\|- S = { y e. _om \| ( F ` suc y ) C. ( F ` y ) }
5		isf32lem.e	\|- J = ( u e. _om \|-> ( iota_ v e. S ( v i^i S ) ~~ u ) )
6		isf32lem.f	\|- K = ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J )
7	6	fveq1i	\|- ( K ` A ) = ( ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A )
8	4	ssrab3	\|- S C_ _om
9	1 2 3 4	isf32lem5	\|- ( ph -> -. S e. Fin )
10	5	fin23lem22	\|- ( ( S C_ _om /\ -. S e. Fin ) -> J : _om -1-1-onto-> S )
11	8 9 10	sylancr	\|- ( ph -> J : _om -1-1-onto-> S )
12		f1of	\|- ( J : _om -1-1-onto-> S -> J : _om --> S )
13	11 12	syl	\|- ( ph -> J : _om --> S )
14		fvco3	\|- ( ( J : _om --> S /\ A e. _om ) -> ( ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) )
15	13 14	sylan	\|- ( ( ph /\ A e. _om ) -> ( ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) )
16	13	ffvelcdmda	\|- ( ( ph /\ A e. _om ) -> ( J ` A ) e. S )
17		fveq2	\|- ( w = ( J ` A ) -> ( F ` w ) = ( F ` ( J ` A ) ) )
18		suceq	\|- ( w = ( J ` A ) -> suc w = suc ( J ` A ) )
19	18	fveq2d	\|- ( w = ( J ` A ) -> ( F ` suc w ) = ( F ` suc ( J ` A ) ) )
20	17 19	difeq12d	\|- ( w = ( J ` A ) -> ( ( F ` w ) \ ( F ` suc w ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
21		eqid	\|- ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) = ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) )
22		fvex	\|- ( F ` ( J ` A ) ) e. _V
23	22	difexi	\|- ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) e. _V
24	20 21 23	fvmpt	\|- ( ( J ` A ) e. S -> ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
25	16 24	syl	\|- ( ( ph /\ A e. _om ) -> ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) ` ( J ` A ) ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
26	15 25	eqtrd	\|- ( ( ph /\ A e. _om ) -> ( ( ( w e. S \|-> ( ( F ` w ) \ ( F ` suc w ) ) ) o. J ) ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
27	7 26	eqtrid	\|- ( ( ph /\ A e. _om ) -> ( K ` A ) = ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) )
28	1	adantr	\|- ( ( ph /\ A e. _om ) -> F : _om --> ~P G )
29	8 16	sselid	\|- ( ( ph /\ A e. _om ) -> ( J ` A ) e. _om )
30	28 29	ffvelcdmd	\|- ( ( ph /\ A e. _om ) -> ( F ` ( J ` A ) ) e. ~P G )
31	30	elpwid	\|- ( ( ph /\ A e. _om ) -> ( F ` ( J ` A ) ) C_ G )
32	31	ssdifssd	\|- ( ( ph /\ A e. _om ) -> ( ( F ` ( J ` A ) ) \ ( F ` suc ( J ` A ) ) ) C_ G )
33	27 32	eqsstrd	\|- ( ( ph /\ A e. _om ) -> ( K ` A ) C_ G )

Metamath Proof Explorer

Theorem isf32lem8

Proof