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
|- F/ n ph
smfpimcclem.z
|- Z e. V
smfpimcclem.s
|- ( ph -> S e. W )
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 )
smfpimcclem.h
|- H = ( n e. Z |-> ( C ` { s e. S | ( `' ( F ` n ) " A ) = ( s i^i dom ( F ` n ) ) } ) )
Assertion smfpimcclem
|- ( ph -> E. h ( h : Z --> S /\ A. n e. Z ( `' ( F ` n ) " A ) = ( ( h ` n ) i^i dom ( F ` n ) ) ) )

Proof

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