Metamath Proof Explorer

Theorem srepdflem1

Description: Lemma for srepdf . (Contributed by BTernaryTau, 30-Sep-2026)

Ref Expression
Hypotheses srepdflem1.1 
|- F/ w ph
srepdflem1.2 
|- ( ph -> A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
srepdflem1.3 
|- F = ( G |` x )
srepdflem1.4 
|- G = { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
Assertion srepdflem1 
|- ( ( ph /\ z e. M ) -> ( E. w e. M ( w e. x /\ A. y ps ) <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )

Proof

Step Hyp Ref Expression
1 srepdflem1.1 
 |-  F/ w ph
2 srepdflem1.2 
 |-  ( ph -> A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
3 srepdflem1.3 
 |-  F = ( G |` x )
4 srepdflem1.4 
 |-  G = { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
5 nfv 
 |-  F/ w z e. M
6 1 5 nfan 
 |-  F/ w ( ph /\ z e. M )
7 3anass 
 |-  ( ( w e. M /\ w e. x /\ A. y ps ) <-> ( w e. M /\ ( w e. x /\ A. y ps ) ) )
8 7 baibr 
 |-  ( w e. M -> ( ( w e. x /\ A. y ps ) <-> ( w e. M /\ w e. x /\ A. y ps ) ) )
9 simp2 
 |-  ( ( w e. M /\ w e. x /\ A. y ps ) -> w e. x )
10 9 a1i 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) -> w e. x ) )
11 ibar 
 |-  ( z e. M -> ( ( w e. M /\ w e. x /\ A. y ps ) <-> ( z e. M /\ ( w e. M /\ w e. x /\ A. y ps ) ) ) )
12 nfa1 
 |-  F/ y A. y ps
13 rexex 
 |-  ( E. y e. M A. z e. M ( A. y ps -> z = y ) -> E. y A. z e. M ( A. y ps -> z = y ) )
14 13 ralimi 
 |-  ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> A. w e. M E. y A. z e. M ( A. y ps -> z = y ) )
15 2 14 syl 
 |-  ( ph -> A. w e. M E. y A. z e. M ( A. y ps -> z = y ) )
16 4 reseq1i 
 |-  ( G |` x ) = ( { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } |` x )
17 3 16 eqtri 
 |-  F = ( { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } |` x )
18 12 15 17 fwfffunres 
 |-  ( ph -> ( ( z e. M /\ ( w e. M /\ w e. x /\ A. y ps ) ) <-> ( w e. dom F /\ ( F ` w ) = z ) ) )
19 12 rmo2i 
 |-  ( E. y e. M A. z e. M ( A. y ps -> z = y ) -> E* z e. M A. y ps )
20 19 ralimi 
 |-  ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> A. w e. M E* z e. M A. y ps )
21 funopab 
 |-  ( Fun { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } <-> A. w E* z ( w e. M /\ z e. M /\ A. y ps ) )
22 4 funeqi 
 |-  ( Fun G <-> Fun { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } )
23 2reu5lem2 
 |-  ( A. w e. M E* z e. M A. y ps <-> A. w E* z ( w e. M /\ z e. M /\ A. y ps ) )
24 21 22 23 3bitr4i 
 |-  ( Fun G <-> A. w e. M E* z e. M A. y ps )
25 20 24 sylibr 
 |-  ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> Fun G )
26 funres 
 |-  ( Fun G -> Fun ( G |` x ) )
27 2 25 26 3syl 
 |-  ( ph -> Fun ( G |` x ) )
28 3 funeqi 
 |-  ( Fun F <-> Fun ( G |` x ) )
29 27 28 sylibr 
 |-  ( ph -> Fun F )
30 29 3biant1d 
 |-  ( ph -> ( ( w e. dom F /\ ( F ` w ) = z ) <-> ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
31 18 30 bitrd 
 |-  ( ph -> ( ( z e. M /\ ( w e. M /\ w e. x /\ A. y ps ) ) <-> ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
32 11 31 sylan9bbr 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) <-> ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
33 nfv 
 |-  F/ y w e. M
34 nfv 
 |-  F/ y z e. M
35 33 34 12 nf3an 
 |-  F/ y ( w e. M /\ z e. M /\ A. y ps )
36 35 nfopab 
 |-  F/_ y { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
37 4 36 nfcxfr 
 |-  F/_ y G
38 nfcv 
 |-  F/_ y x
39 37 38 nfres 
 |-  F/_ y ( G |` x )
40 3 39 nfcxfr 
 |-  F/_ y F
41 40 nffun 
 |-  F/ y Fun F
42 40 nfdm 
 |-  F/_ y dom F
43 42 nfcri 
 |-  F/ y w e. dom F
44 nfcv 
 |-  F/_ y w
45 40 44 nffv 
 |-  F/_ y ( F ` w )
46 45 nfeq1 
 |-  F/ y ( F ` w ) = z
47 41 43 46 nf3an 
 |-  F/ y ( Fun F /\ w e. dom F /\ ( F ` w ) = z )
48 47 19.3 
 |-  ( A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) <-> ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) )
49 32 48 bitr4di 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) <-> A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
50 49 biimpd 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) -> A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
51 10 50 jcad 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) -> ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
52 49 biimprd 
 |-  ( ( ph /\ z e. M ) -> ( A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) -> ( w e. M /\ w e. x /\ A. y ps ) ) )
53 52 adantld 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) -> ( w e. M /\ w e. x /\ A. y ps ) ) )
54 51 53 impbid 
 |-  ( ( ph /\ z e. M ) -> ( ( w e. M /\ w e. x /\ A. y ps ) <-> ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
55 8 54 sylan9bbr 
 |-  ( ( ( ph /\ z e. M ) /\ w e. M ) -> ( ( w e. x /\ A. y ps ) <-> ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
56 6 55 rexbida 
 |-  ( ( ph /\ z e. M ) -> ( E. w e. M ( w e. x /\ A. y ps ) <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )