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 ) ) |