Metamath Proof Explorer

Theorem 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 ) )