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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 snex
 |-  { 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 syl5bir
 |-  ( 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 ) )