Step |
Hyp |
Ref |
Expression |
1 |
|
smfpimcclem.n |
|- F/ n ph |
2 |
|
smfpimcclem.z |
|- Z e. V |
3 |
|
smfpimcclem.s |
|- ( ph -> S e. W ) |
4 |
|
smfpimcclem.c |
|- ( ( ph /\ y e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) -> ( C ` y ) e. y ) |
5 |
|
smfpimcclem.h |
|- H = ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
6 |
|
nfcv |
|- F/_ s S |
7 |
6
|
ssrab2f |
|- { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } C_ S |
8 |
|
eqid |
|- { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } |
9 |
8 3
|
rabexd |
|- ( ph -> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. _V ) |
10 |
9
|
adantr |
|- ( ( ph /\ n e. Z ) -> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. _V ) |
11 |
|
simpl |
|- ( ( ph /\ n e. Z ) -> ph ) |
12 |
|
simpr |
|- ( ( ph /\ n e. Z ) -> n e. Z ) |
13 |
|
eqid |
|- ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) = ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) |
14 |
13
|
elrnmpt1 |
|- ( ( n e. Z /\ { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. _V ) -> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
15 |
12 10 14
|
syl2anc |
|- ( ( ph /\ n e. Z ) -> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
16 |
11 15
|
jca |
|- ( ( ph /\ n e. Z ) -> ( ph /\ { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) ) |
17 |
|
eleq1 |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> ( y e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) <-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) ) |
18 |
17
|
anbi2d |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> ( ( ph /\ y e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) <-> ( ph /\ { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) ) ) |
19 |
|
fveq2 |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> ( C ` y ) = ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
20 |
|
id |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) |
21 |
19 20
|
eleq12d |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> ( ( C ` y ) e. y <-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
22 |
18 21
|
imbi12d |
|- ( y = { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } -> ( ( ( ph /\ y e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) -> ( C ` y ) e. y ) <-> ( ( ph /\ { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) -> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) ) |
23 |
22 4
|
vtoclg |
|- ( { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. _V -> ( ( ph /\ { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } e. ran ( n e. Z |-> { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) -> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
24 |
10 16 23
|
sylc |
|- ( ( ph /\ n e. Z ) -> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) |
25 |
7 24
|
sselid |
|- ( ( ph /\ n e. Z ) -> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. S ) |
26 |
1 25 5
|
fmptdf |
|- ( ph -> H : Z --> S ) |
27 |
|
nfcv |
|- F/_ s C |
28 |
|
nfrab1 |
|- F/_ s { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } |
29 |
27 28
|
nffv |
|- F/_ s ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) |
30 |
|
nfcv |
|- F/_ s ( `' ( F ` n ) " A ) |
31 |
|
nfcv |
|- F/_ s dom ( F ` n ) |
32 |
29 31
|
nfin |
|- F/_ s ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) |
33 |
30 32
|
nfeq |
|- F/ s ( `' ( F ` n ) " A ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) |
34 |
|
ineq1 |
|- ( s = ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) -> ( s i^i dom ( F ` n ) ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) |
35 |
34
|
eqeq2d |
|- ( s = ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) -> ( ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) <-> ( `' ( F ` n ) " A ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) ) |
36 |
29 6 33 35
|
elrabf |
|- ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } <-> ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. S /\ ( `' ( F ` n ) " A ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) ) |
37 |
24 36
|
sylib |
|- ( ( ph /\ n e. Z ) -> ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. S /\ ( `' ( F ` n ) " A ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) ) |
38 |
37
|
simprd |
|- ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " A ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) |
39 |
5
|
a1i |
|- ( ph -> H = ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) ) |
40 |
24
|
elexd |
|- ( ( ph /\ n e. Z ) -> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) e. _V ) |
41 |
39 40
|
fvmpt2d |
|- ( ( ph /\ n e. Z ) -> ( H ` n ) = ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
42 |
41
|
ineq1d |
|- ( ( ph /\ n e. Z ) -> ( ( H ` n ) i^i dom ( F ` n ) ) = ( ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) i^i dom ( F ` n ) ) ) |
43 |
38 42
|
eqtr4d |
|- ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) |
44 |
43
|
ex |
|- ( ph -> ( n e. Z -> ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) ) |
45 |
1 44
|
ralrimi |
|- ( ph -> A. n e. Z ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) |
46 |
2
|
elexi |
|- Z e. _V |
47 |
46
|
mptex |
|- ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) e. _V |
48 |
5 47
|
eqeltri |
|- H e. _V |
49 |
|
feq1 |
|- ( h = H -> ( h : Z --> S <-> H : Z --> S ) ) |
50 |
|
nfcv |
|- F/_ n h |
51 |
|
nfmpt1 |
|- F/_ n ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) ) |
52 |
5 51
|
nfcxfr |
|- F/_ n H |
53 |
50 52
|
nfeq |
|- F/ n h = H |
54 |
|
fveq1 |
|- ( h = H -> ( h ` n ) = ( H ` n ) ) |
55 |
54
|
ineq1d |
|- ( h = H -> ( ( h ` n ) i^i dom ( F ` n ) ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) |
56 |
55
|
eqeq2d |
|- ( h = H -> ( ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) <-> ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) ) |
57 |
53 56
|
ralbid |
|- ( h = H -> ( A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) <-> A. n e. Z ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) ) |
58 |
49 57
|
anbi12d |
|- ( h = H -> ( ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) <-> ( H : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) ) ) |
59 |
48 58
|
spcev |
|- ( ( H : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( H ` n ) i^i dom ( F ` n ) ) ) -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) |
60 |
26 45 59
|
syl2anc |
|- ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) ) |