fin23lem34

Description: Lemma for fin23 . Establish induction invariants on Y which parameterizes our contradictory chain of subsets. In this section, h is the hypothetically assumed family of subsets, g is the ground set, and i is the induction function constructed in the previous section. (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	fin23lem34	\|- ( ( ph /\ A e. _om ) -> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) )

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 = (/) -> ( Y ` a ) = ( Y ` (/) ) )
7		f1eq1	\|- ( ( Y ` a ) = ( Y ` (/) ) -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` (/) ) : _om -1-1-> _V ) )
8	6 7	syl	\|- ( a = (/) -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` (/) ) : _om -1-1-> _V ) )
9	6	rneqd	\|- ( a = (/) -> ran ( Y ` a ) = ran ( Y ` (/) ) )
10	9	unieqd	\|- ( a = (/) -> U. ran ( Y ` a ) = U. ran ( Y ` (/) ) )
11	10	sseq1d	\|- ( a = (/) -> ( U. ran ( Y ` a ) C_ G <-> U. ran ( Y ` (/) ) C_ G ) )
12	8 11	anbi12d	\|- ( a = (/) -> ( ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) <-> ( ( Y ` (/) ) : _om -1-1-> _V /\ U. ran ( Y ` (/) ) C_ G ) ) )
13	12	imbi2d	\|- ( a = (/) -> ( ( ph -> ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) ) <-> ( ph -> ( ( Y ` (/) ) : _om -1-1-> _V /\ U. ran ( Y ` (/) ) C_ G ) ) ) )
14		fveq2	\|- ( a = b -> ( Y ` a ) = ( Y ` b ) )
15		f1eq1	\|- ( ( Y ` a ) = ( Y ` b ) -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` b ) : _om -1-1-> _V ) )
16	14 15	syl	\|- ( a = b -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` b ) : _om -1-1-> _V ) )
17	14	rneqd	\|- ( a = b -> ran ( Y ` a ) = ran ( Y ` b ) )
18	17	unieqd	\|- ( a = b -> U. ran ( Y ` a ) = U. ran ( Y ` b ) )
19	18	sseq1d	\|- ( a = b -> ( U. ran ( Y ` a ) C_ G <-> U. ran ( Y ` b ) C_ G ) )
20	16 19	anbi12d	\|- ( a = b -> ( ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) <-> ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) )
21	20	imbi2d	\|- ( a = b -> ( ( ph -> ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) ) <-> ( ph -> ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) ) )
22		fveq2	\|- ( a = suc b -> ( Y ` a ) = ( Y ` suc b ) )
23		f1eq1	\|- ( ( Y ` a ) = ( Y ` suc b ) -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` suc b ) : _om -1-1-> _V ) )
24	22 23	syl	\|- ( a = suc b -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` suc b ) : _om -1-1-> _V ) )
25	22	rneqd	\|- ( a = suc b -> ran ( Y ` a ) = ran ( Y ` suc b ) )
26	25	unieqd	\|- ( a = suc b -> U. ran ( Y ` a ) = U. ran ( Y ` suc b ) )
27	26	sseq1d	\|- ( a = suc b -> ( U. ran ( Y ` a ) C_ G <-> U. ran ( Y ` suc b ) C_ G ) )
28	24 27	anbi12d	\|- ( a = suc b -> ( ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) <-> ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) ) )
29	28	imbi2d	\|- ( a = suc b -> ( ( ph -> ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) ) <-> ( ph -> ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) ) ) )
30		fveq2	\|- ( a = A -> ( Y ` a ) = ( Y ` A ) )
31		f1eq1	\|- ( ( Y ` a ) = ( Y ` A ) -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` A ) : _om -1-1-> _V ) )
32	30 31	syl	\|- ( a = A -> ( ( Y ` a ) : _om -1-1-> _V <-> ( Y ` A ) : _om -1-1-> _V ) )
33	30	rneqd	\|- ( a = A -> ran ( Y ` a ) = ran ( Y ` A ) )
34	33	unieqd	\|- ( a = A -> U. ran ( Y ` a ) = U. ran ( Y ` A ) )
35	34	sseq1d	\|- ( a = A -> ( U. ran ( Y ` a ) C_ G <-> U. ran ( Y ` A ) C_ G ) )
36	32 35	anbi12d	\|- ( a = A -> ( ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) <-> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) ) )
37	36	imbi2d	\|- ( a = A -> ( ( ph -> ( ( Y ` a ) : _om -1-1-> _V /\ U. ran ( Y ` a ) C_ G ) ) <-> ( ph -> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) ) ) )
38	5	fveq1i	\|- ( Y ` (/) ) = ( ( rec ( i , h ) \|` _om ) ` (/) )
39		fr0g	\|- ( h e. _V -> ( ( rec ( i , h ) \|` _om ) ` (/) ) = h )
40	39	elv	\|- ( ( rec ( i , h ) \|` _om ) ` (/) ) = h
41	38 40	eqtri	\|- ( Y ` (/) ) = h
42		f1eq1	\|- ( ( Y ` (/) ) = h -> ( ( Y ` (/) ) : _om -1-1-> _V <-> h : _om -1-1-> _V ) )
43	41 42	ax-mp	\|- ( ( Y ` (/) ) : _om -1-1-> _V <-> h : _om -1-1-> _V )
44	41	rneqi	\|- ran ( Y ` (/) ) = ran h
45	44	unieqi	\|- U. ran ( Y ` (/) ) = U. ran h
46	45	sseq1i	\|- ( U. ran ( Y ` (/) ) C_ G <-> U. ran h C_ G )
47	43 46	anbi12i	\|- ( ( ( Y ` (/) ) : _om -1-1-> _V /\ U. ran ( Y ` (/) ) C_ G ) <-> ( h : _om -1-1-> _V /\ U. ran h C_ G ) )
48	2 3 47	sylanbrc	\|- ( ph -> ( ( Y ` (/) ) : _om -1-1-> _V /\ U. ran ( Y ` (/) ) C_ G ) )
49		fvex	\|- ( Y ` b ) e. _V
50		f1eq1	\|- ( j = ( Y ` b ) -> ( j : _om -1-1-> _V <-> ( Y ` b ) : _om -1-1-> _V ) )
51		rneq	\|- ( j = ( Y ` b ) -> ran j = ran ( Y ` b ) )
52	51	unieqd	\|- ( j = ( Y ` b ) -> U. ran j = U. ran ( Y ` b ) )
53	52	sseq1d	\|- ( j = ( Y ` b ) -> ( U. ran j C_ G <-> U. ran ( Y ` b ) C_ G ) )
54	50 53	anbi12d	\|- ( j = ( Y ` b ) -> ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) <-> ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) )
55		fveq2	\|- ( j = ( Y ` b ) -> ( i ` j ) = ( i ` ( Y ` b ) ) )
56		f1eq1	\|- ( ( i ` j ) = ( i ` ( Y ` b ) ) -> ( ( i ` j ) : _om -1-1-> _V <-> ( i ` ( Y ` b ) ) : _om -1-1-> _V ) )
57	55 56	syl	\|- ( j = ( Y ` b ) -> ( ( i ` j ) : _om -1-1-> _V <-> ( i ` ( Y ` b ) ) : _om -1-1-> _V ) )
58	55	rneqd	\|- ( j = ( Y ` b ) -> ran ( i ` j ) = ran ( i ` ( Y ` b ) ) )
59	58	unieqd	\|- ( j = ( Y ` b ) -> U. ran ( i ` j ) = U. ran ( i ` ( Y ` b ) ) )
60	59 52	psseq12d	\|- ( j = ( Y ` b ) -> ( U. ran ( i ` j ) C. U. ran j <-> U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) )
61	57 60	anbi12d	\|- ( j = ( Y ` b ) -> ( ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) <-> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) ) )
62	54 61	imbi12d	\|- ( j = ( Y ` b ) -> ( ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) <-> ( ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) ) ) )
63	49 62	spcv	\|- ( 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 ) ) -> ( ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) ) )
64	4 63	syl	\|- ( ph -> ( ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) ) )
65	64	imp	\|- ( ( ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) )
66		pssss	\|- ( U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) -> U. ran ( i ` ( Y ` b ) ) C_ U. ran ( Y ` b ) )
67		sstr	\|- ( ( U. ran ( i ` ( Y ` b ) ) C_ U. ran ( Y ` b ) /\ U. ran ( Y ` b ) C_ G ) -> U. ran ( i ` ( Y ` b ) ) C_ G )
68	66 67	sylan	\|- ( ( U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) /\ U. ran ( Y ` b ) C_ G ) -> U. ran ( i ` ( Y ` b ) ) C_ G )
69	68	expcom	\|- ( U. ran ( Y ` b ) C_ G -> ( U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) -> U. ran ( i ` ( Y ` b ) ) C_ G ) )
70	69	anim2d	\|- ( U. ran ( Y ` b ) C_ G -> ( ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) ) )
71	70	ad2antll	\|- ( ( ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C. U. ran ( Y ` b ) ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) ) )
72	65 71	mpd	\|- ( ( ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) )
73	72	3adant1	\|- ( ( b e. _om /\ ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) )
74		frsuc	\|- ( b e. _om -> ( ( rec ( i , h ) \|` _om ) ` suc b ) = ( i ` ( ( rec ( i , h ) \|` _om ) ` b ) ) )
75	5	fveq1i	\|- ( Y ` suc b ) = ( ( rec ( i , h ) \|` _om ) ` suc b )
76	5	fveq1i	\|- ( Y ` b ) = ( ( rec ( i , h ) \|` _om ) ` b )
77	76	fveq2i	\|- ( i ` ( Y ` b ) ) = ( i ` ( ( rec ( i , h ) \|` _om ) ` b ) )
78	74 75 77	3eqtr4g	\|- ( b e. _om -> ( Y ` suc b ) = ( i ` ( Y ` b ) ) )
79		f1eq1	\|- ( ( Y ` suc b ) = ( i ` ( Y ` b ) ) -> ( ( Y ` suc b ) : _om -1-1-> _V <-> ( i ` ( Y ` b ) ) : _om -1-1-> _V ) )
80		rneq	\|- ( ( Y ` suc b ) = ( i ` ( Y ` b ) ) -> ran ( Y ` suc b ) = ran ( i ` ( Y ` b ) ) )
81	80	unieqd	\|- ( ( Y ` suc b ) = ( i ` ( Y ` b ) ) -> U. ran ( Y ` suc b ) = U. ran ( i ` ( Y ` b ) ) )
82	81	sseq1d	\|- ( ( Y ` suc b ) = ( i ` ( Y ` b ) ) -> ( U. ran ( Y ` suc b ) C_ G <-> U. ran ( i ` ( Y ` b ) ) C_ G ) )
83	79 82	anbi12d	\|- ( ( Y ` suc b ) = ( i ` ( Y ` b ) ) -> ( ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) <-> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) ) )
84	78 83	syl	\|- ( b e. _om -> ( ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) <-> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) ) )
85	84	3ad2ant1	\|- ( ( b e. _om /\ ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) <-> ( ( i ` ( Y ` b ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` b ) ) C_ G ) ) )
86	73 85	mpbird	\|- ( ( b e. _om /\ ph /\ ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) )
87	86	3exp	\|- ( b e. _om -> ( ph -> ( ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) -> ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) ) ) )
88	87	a2d	\|- ( b e. _om -> ( ( ph -> ( ( Y ` b ) : _om -1-1-> _V /\ U. ran ( Y ` b ) C_ G ) ) -> ( ph -> ( ( Y ` suc b ) : _om -1-1-> _V /\ U. ran ( Y ` suc b ) C_ G ) ) ) )
89	13 21 29 37 48 88	finds	\|- ( A e. _om -> ( ph -> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) ) )
90	89	impcom	\|- ( ( ph /\ A e. _om ) -> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) )

Metamath Proof Explorer

Theorem fin23lem34

Proof