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