Metamath Proof Explorer

Theorem modelaxreplem3

Description: Lemma for modelaxrep . We show that the consequent of Replacement is satisfied with ran F as the value of y . (Contributed by Eric Schmidt, 29-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 modelaxreplem.1 
 |-  ( ps -> x C_ M )
2 modelaxreplem.2 
 |-  ( ps -> A. f ( ( Fun f /\ dom f e. M /\ ran f C_ M ) -> ran f e. M ) )
3 modelaxreplem.3 
 |-  ( ps -> (/) e. M )
4 modelaxreplem.4 
 |-  ( ps -> x e. M )
5 modelaxreplem2.5 
 |-  F/ w ps
6 modelaxreplem2.6 
 |-  F/ z ps
7 modelaxreplem2.7 
 |-  F/_ z F
8 modelaxreplem2.8 
 |-  F = { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) }
9 modelaxreplem2.9 
 |-  ( ps -> ( w e. M -> E. y e. M A. z e. M ( A. y ph -> z = y ) ) )
10 1 2 3 4 5 6 7 8 9 modelaxreplem2 
 |-  ( ps -> ran F e. M )
11 1 sseld 
 |-  ( ps -> ( w e. x -> w e. M ) )
12 11 pm4.71rd 
 |-  ( ps -> ( w e. x <-> ( w e. M /\ w e. x ) ) )
13 12 anbi1d 
 |-  ( ps -> ( ( w e. x /\ ( z e. M /\ A. y ph ) ) <-> ( ( w e. M /\ w e. x ) /\ ( z e. M /\ A. y ph ) ) ) )
14 an12 
 |-  ( ( ( w e. M /\ w e. x ) /\ ( z e. M /\ A. y ph ) ) <-> ( z e. M /\ ( ( w e. M /\ w e. x ) /\ A. y ph ) ) )
15 anass 
 |-  ( ( ( w e. M /\ w e. x ) /\ A. y ph ) <-> ( w e. M /\ ( w e. x /\ A. y ph ) ) )
16 15 anbi2i 
 |-  ( ( z e. M /\ ( ( w e. M /\ w e. x ) /\ A. y ph ) ) <-> ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) )
17 14 16 bitri 
 |-  ( ( ( w e. M /\ w e. x ) /\ ( z e. M /\ A. y ph ) ) <-> ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) )
18 13 17 bitrdi 
 |-  ( ps -> ( ( w e. x /\ ( z e. M /\ A. y ph ) ) <-> ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) ) )
19 5 18 exbid 
 |-  ( ps -> ( E. w ( w e. x /\ ( z e. M /\ A. y ph ) ) <-> E. w ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) ) )
20 8 rneqi 
 |-  ran F = ran { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) }
21 rnopab 
 |-  ran { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) } = { z | E. w ( w e. x /\ ( z e. M /\ A. y ph ) ) }
22 20 21 eqtri 
 |-  ran F = { z | E. w ( w e. x /\ ( z e. M /\ A. y ph ) ) }
23 22 eqabri 
 |-  ( z e. ran F <-> E. w ( w e. x /\ ( z e. M /\ A. y ph ) ) )
24 df-rex 
 |-  ( E. w e. M ( w e. x /\ A. y ph ) <-> E. w ( w e. M /\ ( w e. x /\ A. y ph ) ) )
25 24 anbi2i 
 |-  ( ( z e. M /\ E. w e. M ( w e. x /\ A. y ph ) ) <-> ( z e. M /\ E. w ( w e. M /\ ( w e. x /\ A. y ph ) ) ) )
26 19.42v 
 |-  ( E. w ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) <-> ( z e. M /\ E. w ( w e. M /\ ( w e. x /\ A. y ph ) ) ) )
27 25 26 bitr4i 
 |-  ( ( z e. M /\ E. w e. M ( w e. x /\ A. y ph ) ) <-> E. w ( z e. M /\ ( w e. M /\ ( w e. x /\ A. y ph ) ) ) )
28 19 23 27 3bitr4g 
 |-  ( ps -> ( z e. ran F <-> ( z e. M /\ E. w e. M ( w e. x /\ A. y ph ) ) ) )
29 28 baibd 
 |-  ( ( ps /\ z e. M ) -> ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) )
30 6 29 ralrimia 
 |-  ( ps -> A. z e. M ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) )
31 7 nfrn 
 |-  F/_ z ran F
32 sbcralt 
 |-  ( ( ran F e. M /\ F/_ z ran F ) -> ( [. ran F / y ]. A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> A. z e. M [. ran F / y ]. ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
33 31 32 mpan2 
 |-  ( ran F e. M -> ( [. ran F / y ]. A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> A. z e. M [. ran F / y ]. ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
34 31 nfel1 
 |-  F/ z ran F e. M
35 sbcbig 
 |-  ( ran F e. M -> ( [. ran F / y ]. ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> ( [. ran F / y ]. z e. y <-> [. ran F / y ]. E. w e. M ( w e. x /\ A. y ph ) ) ) )
36 sbcel2gv 
 |-  ( ran F e. M -> ( [. ran F / y ]. z e. y <-> z e. ran F ) )
37 nfcv 
 |-  F/_ y M
38 nfv 
 |-  F/ y w e. x
39 nfa1 
 |-  F/ y A. y ph
40 38 39 nfan 
 |-  F/ y ( w e. x /\ A. y ph )
41 37 40 nfrexw 
 |-  F/ y E. w e. M ( w e. x /\ A. y ph )
42 41 sbcgf 
 |-  ( ran F e. M -> ( [. ran F / y ]. E. w e. M ( w e. x /\ A. y ph ) <-> E. w e. M ( w e. x /\ A. y ph ) ) )
43 36 42 bibi12d 
 |-  ( ran F e. M -> ( ( [. ran F / y ]. z e. y <-> [. ran F / y ]. E. w e. M ( w e. x /\ A. y ph ) ) <-> ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
44 35 43 bitrd 
 |-  ( ran F e. M -> ( [. ran F / y ]. ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
45 34 44 ralbid 
 |-  ( ran F e. M -> ( A. z e. M [. ran F / y ]. ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> A. z e. M ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
46 33 45 bitrd 
 |-  ( ran F e. M -> ( [. ran F / y ]. A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> A. z e. M ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
47 10 46 syl 
 |-  ( ps -> ( [. ran F / y ]. A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) <-> A. z e. M ( z e. ran F <-> E. w e. M ( w e. x /\ A. y ph ) ) ) )
48 30 47 mpbird 
 |-  ( ps -> [. ran F / y ]. A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) )
49 10 48 rspesbcd 
 |-  ( ps -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) )