Metamath Proof Explorer

Theorem modelaxreplem1

Description: Lemma for modelaxrep . We show that M is closed under taking subsets. (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 )
modelaxreplem1.5 
|- A C_ x
Assertion modelaxreplem1 
|- ( ps -> A 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 modelaxreplem1.5 
 |-  A C_ x
6 eleq1 
 |-  ( A = (/) -> ( A e. M <-> (/) e. M ) )
7 3 6 syl5ibrcom 
 |-  ( ps -> ( A = (/) -> A e. M ) )
8 vex 
 |-  x e. _V
9 8 5 ssexi 
 |-  A e. _V
10 9 0sdom 
 |-  ( (/) ~< A <-> A =/= (/) )
11 ssdomg 
 |-  ( x e. _V -> ( A C_ x -> A ~<_ x ) )
12 8 5 11 mp2 
 |-  A ~<_ x
13 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ x ) -> E. g g : x -onto-> A )
14 12 13 mpan2 
 |-  ( (/) ~< A -> E. g g : x -onto-> A )
15 10 14 sylbir 
 |-  ( A =/= (/) -> E. g g : x -onto-> A )
16 df-fo 
 |-  ( g : x -onto-> A <-> ( g Fn x /\ ran g = A ) )
17 df-fn 
 |-  ( g Fn x <-> ( Fun g /\ dom g = x ) )
18 eleq1 
 |-  ( dom g = x -> ( dom g e. M <-> x e. M ) )
19 4 18 syl5ibrcom 
 |-  ( ps -> ( dom g = x -> dom g e. M ) )
20 19 anim2d 
 |-  ( ps -> ( ( Fun g /\ dom g = x ) -> ( Fun g /\ dom g e. M ) ) )
21 17 20 biimtrid 
 |-  ( ps -> ( g Fn x -> ( Fun g /\ dom g e. M ) ) )
22 5 1 sstrid 
 |-  ( ps -> A C_ M )
23 sseq1 
 |-  ( ran g = A -> ( ran g C_ M <-> A C_ M ) )
24 22 23 syl5ibrcom 
 |-  ( ps -> ( ran g = A -> ran g C_ M ) )
25 df-3an 
 |-  ( ( Fun g /\ dom g e. M /\ ran g C_ M ) <-> ( ( Fun g /\ dom g e. M ) /\ ran g C_ M ) )
26 funeq 
 |-  ( f = g -> ( Fun f <-> Fun g ) )
27 dmeq 
 |-  ( f = g -> dom f = dom g )
28 27 eleq1d 
 |-  ( f = g -> ( dom f e. M <-> dom g e. M ) )
29 rneq 
 |-  ( f = g -> ran f = ran g )
30 29 sseq1d 
 |-  ( f = g -> ( ran f C_ M <-> ran g C_ M ) )
31 26 28 30 3anbi123d 
 |-  ( f = g -> ( ( Fun f /\ dom f e. M /\ ran f C_ M ) <-> ( Fun g /\ dom g e. M /\ ran g C_ M ) ) )
32 29 eleq1d 
 |-  ( f = g -> ( ran f e. M <-> ran g e. M ) )
33 31 32 imbi12d 
 |-  ( f = g -> ( ( ( Fun f /\ dom f e. M /\ ran f C_ M ) -> ran f e. M ) <-> ( ( Fun g /\ dom g e. M /\ ran g C_ M ) -> ran g e. M ) ) )
34 33 spvv 
 |-  ( A. f ( ( Fun f /\ dom f e. M /\ ran f C_ M ) -> ran f e. M ) -> ( ( Fun g /\ dom g e. M /\ ran g C_ M ) -> ran g e. M ) )
35 2 34 syl 
 |-  ( ps -> ( ( Fun g /\ dom g e. M /\ ran g C_ M ) -> ran g e. M ) )
36 25 35 biimtrrid 
 |-  ( ps -> ( ( ( Fun g /\ dom g e. M ) /\ ran g C_ M ) -> ran g e. M ) )
37 21 24 36 syl2and 
 |-  ( ps -> ( ( g Fn x /\ ran g = A ) -> ran g e. M ) )
38 eleq1 
 |-  ( ran g = A -> ( ran g e. M <-> A e. M ) )
39 38 adantl 
 |-  ( ( g Fn x /\ ran g = A ) -> ( ran g e. M <-> A e. M ) )
40 37 39 mpbidi 
 |-  ( ps -> ( ( g Fn x /\ ran g = A ) -> A e. M ) )
41 16 40 biimtrid 
 |-  ( ps -> ( g : x -onto-> A -> A e. M ) )
42 41 exlimdv 
 |-  ( ps -> ( E. g g : x -onto-> A -> A e. M ) )
43 15 42 syl5 
 |-  ( ps -> ( A =/= (/) -> A e. M ) )
44 7 43 pm2.61dne 
 |-  ( ps -> A e. M )