Metamath Proof Explorer

Theorem srepdflem2

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

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

Proof

Step Hyp Ref Expression
1 srepdflem2.1 
 |-  F/ f ph
2 srepdflem2.2 
 |-  F/ w ph
3 srepdflem2.3 
 |-  F/ y ph
4 srepdflem2.4 
 |-  F/ z ph
5 srepdflem2.5 
 |-  ( ph -> x e. M )
6 srepdflem2.6 
 |-  ( ph -> ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) )
7 srepdflem2.7 
 |-  ( ph -> A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
8 srepdflem2.8 
 |-  F = ( G |` x )
9 srepdflem2.9 
 |-  G = { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
10 nfa1 
 |-  F/ y A. y ps
11 10 rmo2i 
 |-  ( E. y e. M A. z e. M ( A. y ps -> z = y ) -> E* z e. M A. y ps )
12 11 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 )
13 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 ) )
14 9 funeqi 
 |-  ( Fun G <-> Fun { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } )
15 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 ) )
16 13 14 15 3bitr4i 
 |-  ( Fun G <-> A. w e. M E* z e. M A. y ps )
17 12 16 sylibr 
 |-  ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> Fun G )
18 resfunexg 
 |-  ( ( Fun G /\ x e. _V ) -> ( G |` x ) e. _V )
19 18 elvd 
 |-  ( Fun G -> ( G |` x ) e. _V )
20 7 17 19 3syl 
 |-  ( ph -> ( G |` x ) e. _V )
21 8 20 eqeltrid 
 |-  ( ph -> F e. _V )
22 elex2 
 |-  ( x e. M -> E. y y e. M )
23 rmoeq 
 |-  E* z e. M z = ( f ` w )
24 simp3 
 |-  ( ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> ( f ` w ) = z )
25 24 eqcomd 
 |-  ( ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = ( f ` w ) )
26 25 spsv 
 |-  ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = ( f ` w ) )
27 26 rmoimi 
 |-  ( E* z e. M z = ( f ` w ) -> E* z e. M A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) )
28 23 27 ax-mp 
 |-  E* z e. M A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z )
29 nfa1 
 |-  F/ y A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z )
30 29 rmo6 
 |-  ( E* z e. M A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) <-> ( E. y y e. M -> E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) ) )
31 28 30 mpbi 
 |-  ( E. y y e. M -> E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
32 5 22 31 3syl 
 |-  ( ph -> E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
33 32 adantr 
 |-  ( ( ph /\ w e. M ) -> E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
34 2 33 ralrimia 
 |-  ( ph -> A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
35 34 6 mpd 
 |-  ( ph -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
36 1 35 alrimi 
 |-  ( ph -> A. f E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
37 nfv 
 |-  F/ y w e. M
38 nfv 
 |-  F/ y z e. M
39 37 38 10 nf3an 
 |-  F/ y ( w e. M /\ z e. M /\ A. y ps )
40 39 nfopab 
 |-  F/_ y { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
41 9 40 nfcxfr 
 |-  F/_ y G
42 nfcv 
 |-  F/_ y x
43 41 42 nfres 
 |-  F/_ y ( G |` x )
44 8 43 nfcxfr 
 |-  F/_ y F
45 44 nfeq2 
 |-  F/ y f = F
46 nfopab2 
 |-  F/_ z { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
47 9 46 nfcxfr 
 |-  F/_ z G
48 nfcv 
 |-  F/_ z x
49 47 48 nfres 
 |-  F/_ z ( G |` x )
50 8 49 nfcxfr 
 |-  F/_ z F
51 50 nfeq2 
 |-  F/ z f = F
52 nfopab1 
 |-  F/_ w { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
53 9 52 nfcxfr 
 |-  F/_ w G
54 nfcv 
 |-  F/_ w x
55 53 54 nfres 
 |-  F/_ w ( G |` x )
56 8 55 nfcxfr 
 |-  F/_ w F
57 56 nfeq2 
 |-  F/ w f = F
58 funeq 
 |-  ( f = F -> ( Fun f <-> Fun F ) )
59 dmeq 
 |-  ( f = F -> dom f = dom F )
60 59 eleq2d 
 |-  ( f = F -> ( w e. dom f <-> w e. dom F ) )
61 fveq1 
 |-  ( f = F -> ( f ` w ) = ( F ` w ) )
62 61 eqeq1d 
 |-  ( f = F -> ( ( f ` w ) = z <-> ( F ` w ) = z ) )
63 58 60 62 3anbi123d 
 |-  ( f = F -> ( ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) <-> ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
64 45 63 albid 
 |-  ( f = F -> ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) <-> A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) )
65 64 anbi2d 
 |-  ( f = F -> ( ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) <-> ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
66 57 65 rexbid 
 |-  ( f = F -> ( E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
67 66 bibi2d 
 |-  ( f = F -> ( ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) ) )
68 51 67 ralbid 
 |-  ( f = F -> ( A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) ) )
69 45 68 rexbid 
 |-  ( f = F -> ( E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) ) )
70 69 spcgv 
 |-  ( F e. _V -> ( A. f E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) ) )
71 21 36 70 sylc 
 |-  ( ph -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) )
72 2 7 8 9 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 ) ) ) )
73 biantr 
 |-  ( ( ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) /\ ( 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 ) ) ) ) -> ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) )
74 72 73 sylan2 
 |-  ( ( ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) /\ ( ph /\ z e. M ) ) -> ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) )
75 74 expcom 
 |-  ( ( ph /\ z e. M ) -> ( ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) -> ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )
76 4 75 ralimdaa 
 |-  ( ph -> ( A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) -> A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )
77 76 a1d 
 |-  ( ph -> ( y e. M -> ( A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) -> A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) ) )
78 3 77 reximdai 
 |-  ( ph -> ( E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun F /\ w e. dom F /\ ( F ` w ) = z ) ) ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )
79 71 78 mpd 
 |-  ( ph -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) )