Metamath Proof Explorer

Theorem mptsnunlem

Description: This is the core of the proof of mptsnun , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypotheses mptsnun.f 
|- F = ( x e. A |-> { x } )
mptsnun.r 
|- R = { u | E. x e. A u = { x } }
Assertion mptsnunlem 
|- ( B C_ A -> B = U. ( F " B ) )

Proof

Step Hyp Ref Expression
1 mptsnun.f 
 |-  F = ( x e. A |-> { x } )
2 mptsnun.r 
 |-  R = { u | E. x e. A u = { x } }
3 df-ima 
 |-  ( F " B ) = ran ( F |` B )
4 1 reseq1i 
 |-  ( F |` B ) = ( ( x e. A |-> { x } ) |` B )
5 resmpt 
 |-  ( B C_ A -> ( ( x e. A |-> { x } ) |` B ) = ( x e. B |-> { x } ) )
6 4 5 eqtrid 
 |-  ( B C_ A -> ( F |` B ) = ( x e. B |-> { x } ) )
7 6 rneqd 
 |-  ( B C_ A -> ran ( F |` B ) = ran ( x e. B |-> { x } ) )
8 rnmptsn 
 |-  ran ( x e. B |-> { x } ) = { u | E. x e. B u = { x } }
9 7 8 eqtrdi 
 |-  ( B C_ A -> ran ( F |` B ) = { u | E. x e. B u = { x } } )
10 3 9 eqtrid 
 |-  ( B C_ A -> ( F " B ) = { u | E. x e. B u = { x } } )
11 10 unieqd 
 |-  ( B C_ A -> U. ( F " B ) = U. { u | E. x e. B u = { x } } )
12 11 eleq2d 
 |-  ( B C_ A -> ( x e. U. ( F " B ) <-> x e. U. { u | E. x e. B u = { x } } ) )
13 eleq1w 
 |-  ( z = x -> ( z e. B <-> x e. B ) )
14 eluniab 
 |-  ( z e. U. { u | E. x e. B u = { x } } <-> E. u ( z e. u /\ E. x e. B u = { x } ) )
15 ancom 
 |-  ( ( z e. u /\ E. x e. B u = { x } ) <-> ( E. x e. B u = { x } /\ z e. u ) )
16 r19.41v 
 |-  ( E. x e. B ( u = { x } /\ z e. u ) <-> ( E. x e. B u = { x } /\ z e. u ) )
17 df-rex 
 |-  ( E. x e. B ( u = { x } /\ z e. u ) <-> E. x ( x e. B /\ ( u = { x } /\ z e. u ) ) )
18 15 16 17 3bitr2i 
 |-  ( ( z e. u /\ E. x e. B u = { x } ) <-> E. x ( x e. B /\ ( u = { x } /\ z e. u ) ) )
19 eleq2 
 |-  ( u = { x } -> ( z e. u <-> z e. { x } ) )
20 19 anbi2d 
 |-  ( u = { x } -> ( ( u = { x } /\ z e. u ) <-> ( u = { x } /\ z e. { x } ) ) )
21 20 adantr 
 |-  ( ( u = { x } /\ z e. u ) -> ( ( u = { x } /\ z e. u ) <-> ( u = { x } /\ z e. { x } ) ) )
22 21 ibi 
 |-  ( ( u = { x } /\ z e. u ) -> ( u = { x } /\ z e. { x } ) )
23 22 anim2i 
 |-  ( ( x e. B /\ ( u = { x } /\ z e. u ) ) -> ( x e. B /\ ( u = { x } /\ z e. { x } ) ) )
24 23 eximi 
 |-  ( E. x ( x e. B /\ ( u = { x } /\ z e. u ) ) -> E. x ( x e. B /\ ( u = { x } /\ z e. { x } ) ) )
25 18 24 sylbi 
 |-  ( ( z e. u /\ E. x e. B u = { x } ) -> E. x ( x e. B /\ ( u = { x } /\ z e. { x } ) ) )
26 an12 
 |-  ( ( x e. B /\ ( u = { x } /\ z e. { x } ) ) <-> ( u = { x } /\ ( x e. B /\ z e. { x } ) ) )
27 26 exbii 
 |-  ( E. x ( x e. B /\ ( u = { x } /\ z e. { x } ) ) <-> E. x ( u = { x } /\ ( x e. B /\ z e. { x } ) ) )
28 exsimpr 
 |-  ( E. x ( u = { x } /\ ( x e. B /\ z e. { x } ) ) -> E. x ( x e. B /\ z e. { x } ) )
29 27 28 sylbi 
 |-  ( E. x ( x e. B /\ ( u = { x } /\ z e. { x } ) ) -> E. x ( x e. B /\ z e. { x } ) )
30 25 29 syl 
 |-  ( ( z e. u /\ E. x e. B u = { x } ) -> E. x ( x e. B /\ z e. { x } ) )
31 30 exlimiv 
 |-  ( E. u ( z e. u /\ E. x e. B u = { x } ) -> E. x ( x e. B /\ z e. { x } ) )
32 14 31 sylbi 
 |-  ( z e. U. { u | E. x e. B u = { x } } -> E. x ( x e. B /\ z e. { x } ) )
33 velsn 
 |-  ( z e. { x } <-> z = x )
34 33 anbi2i 
 |-  ( ( x e. B /\ z e. { x } ) <-> ( x e. B /\ z = x ) )
35 34 exbii 
 |-  ( E. x ( x e. B /\ z e. { x } ) <-> E. x ( x e. B /\ z = x ) )
36 32 35 sylib 
 |-  ( z e. U. { u | E. x e. B u = { x } } -> E. x ( x e. B /\ z = x ) )
37 13 biimparc 
 |-  ( ( x e. B /\ z = x ) -> z e. B )
38 37 exlimiv 
 |-  ( E. x ( x e. B /\ z = x ) -> z e. B )
39 36 38 syl 
 |-  ( z e. U. { u | E. x e. B u = { x } } -> z e. B )
40 13 39 vtoclga 
 |-  ( x e. U. { u | E. x e. B u = { x } } -> x e. B )
41 equid 
 |-  x = x
42 eqid 
 |-  { x } = { x }
43 vsnex 
 |-  { x } e. _V
44 sbcg 
 |-  ( { x } e. _V -> ( [. { x } / u ]. x e. B <-> x e. B ) )
45 43 44 ax-mp 
 |-  ( [. { x } / u ]. x e. B <-> x e. B )
46 eqsbc1 
 |-  ( { x } e. _V -> ( [. { x } / u ]. u = { x } <-> { x } = { x } ) )
47 43 46 ax-mp 
 |-  ( [. { x } / u ]. u = { x } <-> { x } = { x } )
48 19 adantl 
 |-  ( ( x e. B /\ u = { x } ) -> ( z e. u <-> z e. { x } ) )
49 df-rex 
 |-  ( E. x e. B u = { x } <-> E. x ( x e. B /\ u = { x } ) )
50 14 biimpri 
 |-  ( E. u ( z e. u /\ E. x e. B u = { x } ) -> z e. U. { u | E. x e. B u = { x } } )
51 50 19.23bi 
 |-  ( ( z e. u /\ E. x e. B u = { x } ) -> z e. U. { u | E. x e. B u = { x } } )
52 51 expcom 
 |-  ( E. x e. B u = { x } -> ( z e. u -> z e. U. { u | E. x e. B u = { x } } ) )
53 49 52 sylbir 
 |-  ( E. x ( x e. B /\ u = { x } ) -> ( z e. u -> z e. U. { u | E. x e. B u = { x } } ) )
54 53 19.23bi 
 |-  ( ( x e. B /\ u = { x } ) -> ( z e. u -> z e. U. { u | E. x e. B u = { x } } ) )
55 48 54 sylbird 
 |-  ( ( x e. B /\ u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
56 55 sbcth 
 |-  ( { x } e. _V -> [. { x } / u ]. ( ( x e. B /\ u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) ) )
57 43 56 ax-mp 
 |-  [. { x } / u ]. ( ( x e. B /\ u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
58 sbcimg 
 |-  ( { x } e. _V -> ( [. { x } / u ]. ( ( x e. B /\ u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) ) <-> ( [. { x } / u ]. ( x e. B /\ u = { x } ) -> [. { x } / u ]. ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) ) ) )
59 43 58 ax-mp 
 |-  ( [. { x } / u ]. ( ( x e. B /\ u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) ) <-> ( [. { x } / u ]. ( x e. B /\ u = { x } ) -> [. { x } / u ]. ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) ) )
60 57 59 mpbi 
 |-  ( [. { x } / u ]. ( x e. B /\ u = { x } ) -> [. { x } / u ]. ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
61 sbcan 
 |-  ( [. { x } / u ]. ( x e. B /\ u = { x } ) <-> ( [. { x } / u ]. x e. B /\ [. { x } / u ]. u = { x } ) )
62 nfv 
 |-  F/ u z e. { x }
63 nfab1 
 |-  F/_ u { u | E. x e. B u = { x } }
64 63 nfuni 
 |-  F/_ u U. { u | E. x e. B u = { x } }
65 64 nfcri 
 |-  F/ u z e. U. { u | E. x e. B u = { x } }
66 62 65 nfim 
 |-  F/ u ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } )
67 43 66 sbcgfi 
 |-  ( [. { x } / u ]. ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) <-> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
68 60 61 67 3imtr3i 
 |-  ( ( [. { x } / u ]. x e. B /\ [. { x } / u ]. u = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
69 45 47 68 syl2anbr 
 |-  ( ( x e. B /\ { x } = { x } ) -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
70 42 69 mpan2 
 |-  ( x e. B -> ( z e. { x } -> z e. U. { u | E. x e. B u = { x } } ) )
71 33 70 biimtrrid 
 |-  ( x e. B -> ( z = x -> z e. U. { u | E. x e. B u = { x } } ) )
72 eleq1w 
 |-  ( z = x -> ( z e. U. { u | E. x e. B u = { x } } <-> x e. U. { u | E. x e. B u = { x } } ) )
73 71 72 mpbidi 
 |-  ( x e. B -> ( z = x -> x e. U. { u | E. x e. B u = { x } } ) )
74 73 com12 
 |-  ( z = x -> ( x e. B -> x e. U. { u | E. x e. B u = { x } } ) )
75 74 sbimi 
 |-  ( [ x / z ] z = x -> [ x / z ] ( x e. B -> x e. U. { u | E. x e. B u = { x } } ) )
76 equsb3 
 |-  ( [ x / z ] z = x <-> x = x )
77 sbv 
 |-  ( [ x / z ] ( x e. B -> x e. U. { u | E. x e. B u = { x } } ) <-> ( x e. B -> x e. U. { u | E. x e. B u = { x } } ) )
78 75 76 77 3imtr3i 
 |-  ( x = x -> ( x e. B -> x e. U. { u | E. x e. B u = { x } } ) )
79 41 78 ax-mp 
 |-  ( x e. B -> x e. U. { u | E. x e. B u = { x } } )
80 40 79 impbii 
 |-  ( x e. U. { u | E. x e. B u = { x } } <-> x e. B )
81 12 80 bitrdi 
 |-  ( B C_ A -> ( x e. U. ( F " B ) <-> x e. B ) )
82 81 eqrdv 
 |-  ( B C_ A -> U. ( F " B ) = B )
83 82 eqcomd 
 |-  ( B C_ A -> B = U. ( F " B ) )