Metamath Proof Explorer


Theorem smfpimcclem

Description: Lemma for smfpimcc given the choice function C . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfpimcclem.n nφ
smfpimcclem.z ZV
smfpimcclem.s φSW
smfpimcclem.c φyrannZsS|Fn-1A=sdomFnCyy
smfpimcclem.h H=nZCsS|Fn-1A=sdomFn
Assertion smfpimcclem φhh:ZSnZFn-1A=hndomFn

Proof

Step Hyp Ref Expression
1 smfpimcclem.n nφ
2 smfpimcclem.z ZV
3 smfpimcclem.s φSW
4 smfpimcclem.c φyrannZsS|Fn-1A=sdomFnCyy
5 smfpimcclem.h H=nZCsS|Fn-1A=sdomFn
6 nfcv _sS
7 6 ssrab2f sS|Fn-1A=sdomFnS
8 eqid sS|Fn-1A=sdomFn=sS|Fn-1A=sdomFn
9 8 3 rabexd φsS|Fn-1A=sdomFnV
10 9 adantr φnZsS|Fn-1A=sdomFnV
11 simpl φnZφ
12 simpr φnZnZ
13 eqid nZsS|Fn-1A=sdomFn=nZsS|Fn-1A=sdomFn
14 13 elrnmpt1 nZsS|Fn-1A=sdomFnVsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFn
15 12 10 14 syl2anc φnZsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFn
16 11 15 jca φnZφsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFn
17 eleq1 y=sS|Fn-1A=sdomFnyrannZsS|Fn-1A=sdomFnsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFn
18 17 anbi2d y=sS|Fn-1A=sdomFnφyrannZsS|Fn-1A=sdomFnφsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFn
19 fveq2 y=sS|Fn-1A=sdomFnCy=CsS|Fn-1A=sdomFn
20 id y=sS|Fn-1A=sdomFny=sS|Fn-1A=sdomFn
21 19 20 eleq12d y=sS|Fn-1A=sdomFnCyyCsS|Fn-1A=sdomFnsS|Fn-1A=sdomFn
22 18 21 imbi12d y=sS|Fn-1A=sdomFnφyrannZsS|Fn-1A=sdomFnCyyφsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFnCsS|Fn-1A=sdomFnsS|Fn-1A=sdomFn
23 22 4 vtoclg sS|Fn-1A=sdomFnVφsS|Fn-1A=sdomFnrannZsS|Fn-1A=sdomFnCsS|Fn-1A=sdomFnsS|Fn-1A=sdomFn
24 10 16 23 sylc φnZCsS|Fn-1A=sdomFnsS|Fn-1A=sdomFn
25 7 24 sselid φnZCsS|Fn-1A=sdomFnS
26 1 25 5 fmptdf φH:ZS
27 nfcv _sC
28 nfrab1 _ssS|Fn-1A=sdomFn
29 27 28 nffv _sCsS|Fn-1A=sdomFn
30 nfcv _sFn-1A
31 nfcv _sdomFn
32 29 31 nfin _sCsS|Fn-1A=sdomFndomFn
33 30 32 nfeq sFn-1A=CsS|Fn-1A=sdomFndomFn
34 ineq1 s=CsS|Fn-1A=sdomFnsdomFn=CsS|Fn-1A=sdomFndomFn
35 34 eqeq2d s=CsS|Fn-1A=sdomFnFn-1A=sdomFnFn-1A=CsS|Fn-1A=sdomFndomFn
36 29 6 33 35 elrabf CsS|Fn-1A=sdomFnsS|Fn-1A=sdomFnCsS|Fn-1A=sdomFnSFn-1A=CsS|Fn-1A=sdomFndomFn
37 24 36 sylib φnZCsS|Fn-1A=sdomFnSFn-1A=CsS|Fn-1A=sdomFndomFn
38 37 simprd φnZFn-1A=CsS|Fn-1A=sdomFndomFn
39 5 a1i φH=nZCsS|Fn-1A=sdomFn
40 24 elexd φnZCsS|Fn-1A=sdomFnV
41 39 40 fvmpt2d φnZHn=CsS|Fn-1A=sdomFn
42 41 ineq1d φnZHndomFn=CsS|Fn-1A=sdomFndomFn
43 38 42 eqtr4d φnZFn-1A=HndomFn
44 43 ex φnZFn-1A=HndomFn
45 1 44 ralrimi φnZFn-1A=HndomFn
46 2 elexi ZV
47 46 mptex nZCsS|Fn-1A=sdomFnV
48 5 47 eqeltri HV
49 feq1 h=Hh:ZSH:ZS
50 nfcv _nh
51 nfmpt1 _nnZCsS|Fn-1A=sdomFn
52 5 51 nfcxfr _nH
53 50 52 nfeq nh=H
54 fveq1 h=Hhn=Hn
55 54 ineq1d h=HhndomFn=HndomFn
56 55 eqeq2d h=HFn-1A=hndomFnFn-1A=HndomFn
57 53 56 ralbid h=HnZFn-1A=hndomFnnZFn-1A=HndomFn
58 49 57 anbi12d h=Hh:ZSnZFn-1A=hndomFnH:ZSnZFn-1A=HndomFn
59 48 58 spcev H:ZSnZFn-1A=HndomFnhh:ZSnZFn-1A=hndomFn
60 26 45 59 syl2anc φhh:ZSnZFn-1A=hndomFn