Metamath Proof Explorer

Theorem modelaxreplem2

Description: Lemma for modelaxrep . We define a class F and show that the antecedent of Replacement implies that F is a function. We use Replacement (in the form of funex ) to show that F exists. Then we show that, under our hypotheses, the range of F is a member of M . (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 modelaxreplem2 
|- ( ps -> ran F e. M )

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 sseld 
 |-  ( ps -> ( w e. x -> w e. M ) )
11 nfa1 
 |-  F/ y A. y ph
12 11 rmo2i 
 |-  ( E. y e. M A. z e. M ( A. y ph -> z = y ) -> E* z e. M A. y ph )
13 df-rmo 
 |-  ( E* z e. M A. y ph <-> E* z ( z e. M /\ A. y ph ) )
14 12 13 sylib 
 |-  ( E. y e. M A. z e. M ( A. y ph -> z = y ) -> E* z ( z e. M /\ A. y ph ) )
15 9 14 syl6 
 |-  ( ps -> ( w e. M -> E* z ( z e. M /\ A. y ph ) ) )
16 10 15 syld 
 |-  ( ps -> ( w e. x -> E* z ( z e. M /\ A. y ph ) ) )
17 moanimv 
 |-  ( E* z ( w e. x /\ ( z e. M /\ A. y ph ) ) <-> ( w e. x -> E* z ( z e. M /\ A. y ph ) ) )
18 16 17 sylibr 
 |-  ( ps -> E* z ( w e. x /\ ( z e. M /\ A. y ph ) ) )
19 5 18 alrimi 
 |-  ( ps -> A. w E* z ( w e. x /\ ( z e. M /\ A. y ph ) ) )
20 8 funeqi 
 |-  ( Fun F <-> Fun { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) } )
21 funopab 
 |-  ( Fun { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) } <-> A. w E* z ( w e. x /\ ( z e. M /\ A. y ph ) ) )
22 20 21 bitri 
 |-  ( Fun F <-> A. w E* z ( w e. x /\ ( z e. M /\ A. y ph ) ) )
23 19 22 sylibr 
 |-  ( ps -> Fun F )
24 8 dmeqi 
 |-  dom F = dom { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) }
25 dmopabss 
 |-  dom { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) } C_ x
26 24 25 eqsstri 
 |-  dom F C_ x
27 1 2 3 4 26 modelaxreplem1 
 |-  ( ps -> dom F e. M )
28 an12 
 |-  ( ( w e. x /\ ( z e. M /\ A. y ph ) ) <-> ( z e. M /\ ( w e. x /\ A. y ph ) ) )
29 28 opabbii 
 |-  { <. w , z >. | ( w e. x /\ ( z e. M /\ A. y ph ) ) } = { <. w , z >. | ( z e. M /\ ( w e. x /\ A. y ph ) ) }
30 8 29 eqtri 
 |-  F = { <. w , z >. | ( z e. M /\ ( w e. x /\ A. y ph ) ) }
31 30 rneqi 
 |-  ran F = ran { <. w , z >. | ( z e. M /\ ( w e. x /\ A. y ph ) ) }
32 rnopabss 
 |-  ran { <. w , z >. | ( z e. M /\ ( w e. x /\ A. y ph ) ) } C_ M
33 31 32 eqsstri 
 |-  ran F C_ M
34 33 a1i 
 |-  ( ps -> ran F C_ M )
35 funex 
 |-  ( ( Fun F /\ dom F e. M ) -> F e. _V )
36 23 27 35 syl2anc 
 |-  ( ps -> F e. _V )
37 funeq 
 |-  ( f = F -> ( Fun f <-> Fun F ) )
38 dmeq 
 |-  ( f = F -> dom f = dom F )
39 38 eleq1d 
 |-  ( f = F -> ( dom f e. M <-> dom F e. M ) )
40 rneq 
 |-  ( f = F -> ran f = ran F )
41 40 sseq1d 
 |-  ( f = F -> ( ran f C_ M <-> ran F C_ M ) )
42 37 39 41 3anbi123d 
 |-  ( f = F -> ( ( Fun f /\ dom f e. M /\ ran f C_ M ) <-> ( Fun F /\ dom F e. M /\ ran F C_ M ) ) )
43 40 eleq1d 
 |-  ( f = F -> ( ran f e. M <-> ran F e. M ) )
44 42 43 imbi12d 
 |-  ( f = F -> ( ( ( Fun f /\ dom f e. M /\ ran f C_ M ) -> ran f e. M ) <-> ( ( Fun F /\ dom F e. M /\ ran F C_ M ) -> ran F e. M ) ) )
45 44 spcgv 
 |-  ( F e. _V -> ( A. f ( ( Fun f /\ dom f e. M /\ ran f C_ M ) -> ran f e. M ) -> ( ( Fun F /\ dom F e. M /\ ran F C_ M ) -> ran F e. M ) ) )
46 36 2 45 sylc 
 |-  ( ps -> ( ( Fun F /\ dom F e. M /\ ran F C_ M ) -> ran F e. M ) )
47 23 27 34 46 mp3and 
 |-  ( ps -> ran F e. M )