fin23lem36

Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem33.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.f	\|- ( ph -> h : _om -1-1-> _V )
	fin23lem.g	\|- ( ph -> U. ran h C_ G )
	fin23lem.h	\|- ( ph -> A. j ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )
	fin23lem.i	\|- Y = ( rec ( i , h ) \|` _om )
Assertion	fin23lem36	\|- ( ( ( A e. _om /\ B e. _om ) /\ ( B C_ A /\ ph ) ) -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem33.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 ) }
2		fin23lem.f	\|- ( ph -> h : _om -1-1-> _V )
3		fin23lem.g	\|- ( ph -> U. ran h C_ G )
4		fin23lem.h	\|- ( ph -> A. j ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )
5		fin23lem.i	\|- Y = ( rec ( i , h ) \|` _om )
6		fveq2	\|- ( a = B -> ( Y ` a ) = ( Y ` B ) )
7	6	rneqd	\|- ( a = B -> ran ( Y ` a ) = ran ( Y ` B ) )
8	7	unieqd	\|- ( a = B -> U. ran ( Y ` a ) = U. ran ( Y ` B ) )
9	8	sseq1d	\|- ( a = B -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) )
10	9	imbi2d	\|- ( a = B -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) ) )
11		fveq2	\|- ( a = b -> ( Y ` a ) = ( Y ` b ) )
12	11	rneqd	\|- ( a = b -> ran ( Y ` a ) = ran ( Y ` b ) )
13	12	unieqd	\|- ( a = b -> U. ran ( Y ` a ) = U. ran ( Y ` b ) )
14	13	sseq1d	\|- ( a = b -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) )
15	14	imbi2d	\|- ( a = b -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) ) )
16		fveq2	\|- ( a = suc b -> ( Y ` a ) = ( Y ` suc b ) )
17	16	rneqd	\|- ( a = suc b -> ran ( Y ` a ) = ran ( Y ` suc b ) )
18	17	unieqd	\|- ( a = suc b -> U. ran ( Y ` a ) = U. ran ( Y ` suc b ) )
19	18	sseq1d	\|- ( a = suc b -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
20	19	imbi2d	\|- ( a = suc b -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
21		fveq2	\|- ( a = A -> ( Y ` a ) = ( Y ` A ) )
22	21	rneqd	\|- ( a = A -> ran ( Y ` a ) = ran ( Y ` A ) )
23	22	unieqd	\|- ( a = A -> U. ran ( Y ` a ) = U. ran ( Y ` A ) )
24	23	sseq1d	\|- ( a = A -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) )
25	24	imbi2d	\|- ( a = A -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) ) )
26		ssid	\|- U. ran ( Y ` B ) C_ U. ran ( Y ` B )
27	26	2a1i	\|- ( B e. _om -> ( ph -> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) )
28		simprr	\|- ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> ph )
29		simpll	\|- ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> b e. _om )
30	1 2 3 4 5	fin23lem35	\|- ( ( ph /\ b e. _om ) -> U. ran ( Y ` suc b ) C. U. ran ( Y ` b ) )
31	28 29 30	syl2anc	\|- ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> U. ran ( Y ` suc b ) C. U. ran ( Y ` b ) )
32	31	pssssd	\|- ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` b ) )
33		sstr2	\|- ( U. ran ( Y ` suc b ) C_ U. ran ( Y ` b ) -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
34	32 33	syl	\|- ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
35	34	expr	\|- ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( ph -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
36	35	a2d	\|- ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( ( ph -> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) -> ( ph -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
37	10 15 20 25 27 36	findsg	\|- ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( ph -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) )
38	37	impr	\|- ( ( ( A e. _om /\ B e. _om ) /\ ( B C_ A /\ ph ) ) -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) )

Metamath Proof Explorer

Theorem fin23lem36

Proof