Metamath Proof Explorer

Theorem mnurndlem1

Description: Lemma for mnurnd . (Contributed by Rohan Ridenour, 12-Aug-2023)

Ref Expression
Hypotheses mnurndlem1.3 
|- ( ph -> F : A --> U )
mnurndlem1.4 
|- A e. _V
mnurndlem1.6 
|- ( ph -> A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) )
Assertion mnurndlem1 
|- ( ph -> ran F C_ w )

Proof

Step Hyp Ref Expression
1 mnurndlem1.3 
 |-  ( ph -> F : A --> U )
2 mnurndlem1.4 
 |-  A e. _V
3 mnurndlem1.6 
 |-  ( ph -> A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) )
4 1 ffnd 
 |-  ( ph -> F Fn A )
5 vex 
 |-  i e. _V
6 5 prid1 
 |-  i e. { i , { ( F ` i ) , A } }
7 simpr 
 |-  ( ( i e. A /\ v = { i , { ( F ` i ) , A } } ) -> v = { i , { ( F ` i ) , A } } )
8 6 7 eleqtrrid 
 |-  ( ( i e. A /\ v = { i , { ( F ` i ) , A } } ) -> i e. v )
9 eqid 
 |-  ( a e. A |-> { a , { ( F ` a ) , A } } ) = ( a e. A |-> { a , { ( F ` a ) , A } } )
10 id 
 |-  ( i e. A -> i e. A )
11 prex 
 |-  { i , { ( F ` i ) , A } } e. _V
12 11 a1i 
 |-  ( i e. A -> { i , { ( F ` i ) , A } } e. _V )
13 id 
 |-  ( a = i -> a = i )
14 fveq2 
 |-  ( a = i -> ( F ` a ) = ( F ` i ) )
15 14 preq1d 
 |-  ( a = i -> { ( F ` a ) , A } = { ( F ` i ) , A } )
16 13 15 preq12d 
 |-  ( a = i -> { a , { ( F ` a ) , A } } = { i , { ( F ` i ) , A } } )
17 16 adantl 
 |-  ( ( i e. A /\ a = i ) -> { a , { ( F ` a ) , A } } = { i , { ( F ` i ) , A } } )
18 9 10 12 17 rr-elrnmpt3d 
 |-  ( i e. A -> { i , { ( F ` i ) , A } } e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) )
19 8 18 rspcime 
 |-  ( i e. A -> E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v )
20 19 rgen 
 |-  A. i e. A E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v
21 ralim 
 |-  ( A. i e. A ( E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) -> ( A. i e. A E. v e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) i e. v -> A. i e. A E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) ) )
22 3 20 21 mpisyl 
 |-  ( ph -> A. i e. A E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) )
23 prex 
 |-  { a , { ( F ` a ) , A } } e. _V
24 23 rgenw 
 |-  A. a e. A { a , { ( F ` a ) , A } } e. _V
25 eleq2 
 |-  ( u = { a , { ( F ` a ) , A } } -> ( i e. u <-> i e. { a , { ( F ` a ) , A } } ) )
26 unieq 
 |-  ( u = { a , { ( F ` a ) , A } } -> U. u = U. { a , { ( F ` a ) , A } } )
27 26 sseq1d 
 |-  ( u = { a , { ( F ` a ) , A } } -> ( U. u C_ w <-> U. { a , { ( F ` a ) , A } } C_ w ) )
28 25 27 anbi12d 
 |-  ( u = { a , { ( F ` a ) , A } } -> ( ( i e. u /\ U. u C_ w ) <-> ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) )
29 9 28 rexrnmptw 
 |-  ( A. a e. A { a , { ( F ` a ) , A } } e. _V -> ( E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) <-> E. a e. A ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) )
30 24 29 ax-mp 
 |-  ( E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) <-> E. a e. A ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) )
31 simplrl 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> i e. { a , { ( F ` a ) , A } } )
32 simpr 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> i e. A )
33 2 prid2 
 |-  A e. { ( F ` a ) , A }
34 elnotel 
 |-  ( A e. { ( F ` a ) , A } -> -. { ( F ` a ) , A } e. A )
35 33 34 ax-mp 
 |-  -. { ( F ` a ) , A } e. A
36 35 a1i 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> -. { ( F ` a ) , A } e. A )
37 32 36 elnelneq2d 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> -. i = { ( F ` a ) , A } )
38 elpri 
 |-  ( i e. { a , { ( F ` a ) , A } } -> ( i = a \/ i = { ( F ` a ) , A } ) )
39 38 orcomd 
 |-  ( i e. { a , { ( F ` a ) , A } } -> ( i = { ( F ` a ) , A } \/ i = a ) )
40 39 ord 
 |-  ( i e. { a , { ( F ` a ) , A } } -> ( -. i = { ( F ` a ) , A } -> i = a ) )
41 31 37 40 sylc 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> i = a )
42 41 fveq2d 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> ( F ` i ) = ( F ` a ) )
43 simplrr 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> U. { a , { ( F ` a ) , A } } C_ w )
44 vex 
 |-  a e. _V
45 prex 
 |-  { ( F ` a ) , A } e. _V
46 44 45 unipr 
 |-  U. { a , { ( F ` a ) , A } } = ( a u. { ( F ` a ) , A } )
47 46 sseq1i 
 |-  ( U. { a , { ( F ` a ) , A } } C_ w <-> ( a u. { ( F ` a ) , A } ) C_ w )
48 unss 
 |-  ( ( a C_ w /\ { ( F ` a ) , A } C_ w ) <-> ( a u. { ( F ` a ) , A } ) C_ w )
49 48 bicomi 
 |-  ( ( a u. { ( F ` a ) , A } ) C_ w <-> ( a C_ w /\ { ( F ` a ) , A } C_ w ) )
50 49 simprbi 
 |-  ( ( a u. { ( F ` a ) , A } ) C_ w -> { ( F ` a ) , A } C_ w )
51 47 50 sylbi 
 |-  ( U. { a , { ( F ` a ) , A } } C_ w -> { ( F ` a ) , A } C_ w )
52 fvex 
 |-  ( F ` a ) e. _V
53 52 2 prss 
 |-  ( ( ( F ` a ) e. w /\ A e. w ) <-> { ( F ` a ) , A } C_ w )
54 53 bicomi 
 |-  ( { ( F ` a ) , A } C_ w <-> ( ( F ` a ) e. w /\ A e. w ) )
55 54 simplbi 
 |-  ( { ( F ` a ) , A } C_ w -> ( F ` a ) e. w )
56 43 51 55 3syl 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> ( F ` a ) e. w )
57 42 56 eqeltrd 
 |-  ( ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) /\ i e. A ) -> ( F ` i ) e. w )
58 57 ex 
 |-  ( ( a e. A /\ ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) ) -> ( i e. A -> ( F ` i ) e. w ) )
59 58 rexlimiva 
 |-  ( E. a e. A ( i e. { a , { ( F ` a ) , A } } /\ U. { a , { ( F ` a ) , A } } C_ w ) -> ( i e. A -> ( F ` i ) e. w ) )
60 30 59 sylbi 
 |-  ( E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) -> ( i e. A -> ( F ` i ) e. w ) )
61 60 com12 
 |-  ( i e. A -> ( E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) -> ( F ` i ) e. w ) )
62 61 ralimia 
 |-  ( A. i e. A E. u e. ran ( a e. A |-> { a , { ( F ` a ) , A } } ) ( i e. u /\ U. u C_ w ) -> A. i e. A ( F ` i ) e. w )
63 22 62 syl 
 |-  ( ph -> A. i e. A ( F ` i ) e. w )
64 fnfvrnss 
 |-  ( ( F Fn A /\ A. i e. A ( F ` i ) e. w ) -> ran F C_ w )
65 4 63 64 syl2anc 
 |-  ( ph -> ran F C_ w )