Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
|- ( B |`t A ) e. _V |
2 |
|
eltg3 |
|- ( ( B |`t A ) e. _V -> ( x e. ( topGen ` ( B |`t A ) ) <-> E. y ( y C_ ( B |`t A ) /\ x = U. y ) ) ) |
3 |
1 2
|
ax-mp |
|- ( x e. ( topGen ` ( B |`t A ) ) <-> E. y ( y C_ ( B |`t A ) /\ x = U. y ) ) |
4 |
|
simpll |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> B e. V ) |
5 |
|
funmpt |
|- Fun ( x e. B |-> ( x i^i A ) ) |
6 |
5
|
a1i |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> Fun ( x e. B |-> ( x i^i A ) ) ) |
7 |
|
restval |
|- ( ( B e. V /\ A e. W ) -> ( B |`t A ) = ran ( x e. B |-> ( x i^i A ) ) ) |
8 |
7
|
sseq2d |
|- ( ( B e. V /\ A e. W ) -> ( y C_ ( B |`t A ) <-> y C_ ran ( x e. B |-> ( x i^i A ) ) ) ) |
9 |
8
|
biimpa |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> y C_ ran ( x e. B |-> ( x i^i A ) ) ) |
10 |
|
vex |
|- x e. _V |
11 |
10
|
inex1 |
|- ( x i^i A ) e. _V |
12 |
11
|
rgenw |
|- A. x e. B ( x i^i A ) e. _V |
13 |
|
eqid |
|- ( x e. B |-> ( x i^i A ) ) = ( x e. B |-> ( x i^i A ) ) |
14 |
13
|
fnmpt |
|- ( A. x e. B ( x i^i A ) e. _V -> ( x e. B |-> ( x i^i A ) ) Fn B ) |
15 |
|
fnima |
|- ( ( x e. B |-> ( x i^i A ) ) Fn B -> ( ( x e. B |-> ( x i^i A ) ) " B ) = ran ( x e. B |-> ( x i^i A ) ) ) |
16 |
12 14 15
|
mp2b |
|- ( ( x e. B |-> ( x i^i A ) ) " B ) = ran ( x e. B |-> ( x i^i A ) ) |
17 |
9 16
|
sseqtrrdi |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> y C_ ( ( x e. B |-> ( x i^i A ) ) " B ) ) |
18 |
|
ssimaexg |
|- ( ( B e. V /\ Fun ( x e. B |-> ( x i^i A ) ) /\ y C_ ( ( x e. B |-> ( x i^i A ) ) " B ) ) -> E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) ) |
19 |
4 6 17 18
|
syl3anc |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) ) |
20 |
|
df-ima |
|- ( ( x e. B |-> ( x i^i A ) ) " z ) = ran ( ( x e. B |-> ( x i^i A ) ) |` z ) |
21 |
|
resmpt |
|- ( z C_ B -> ( ( x e. B |-> ( x i^i A ) ) |` z ) = ( x e. z |-> ( x i^i A ) ) ) |
22 |
21
|
adantl |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( ( x e. B |-> ( x i^i A ) ) |` z ) = ( x e. z |-> ( x i^i A ) ) ) |
23 |
22
|
rneqd |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ran ( ( x e. B |-> ( x i^i A ) ) |` z ) = ran ( x e. z |-> ( x i^i A ) ) ) |
24 |
20 23
|
syl5eq |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( ( x e. B |-> ( x i^i A ) ) " z ) = ran ( x e. z |-> ( x i^i A ) ) ) |
25 |
24
|
unieqd |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = U. ran ( x e. z |-> ( x i^i A ) ) ) |
26 |
11
|
dfiun3 |
|- U_ x e. z ( x i^i A ) = U. ran ( x e. z |-> ( x i^i A ) ) |
27 |
25 26
|
eqtr4di |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = U_ x e. z ( x i^i A ) ) |
28 |
|
iunin1 |
|- U_ x e. z ( x i^i A ) = ( U_ x e. z x i^i A ) |
29 |
27 28
|
eqtrdi |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) = ( U_ x e. z x i^i A ) ) |
30 |
|
fvex |
|- ( topGen ` B ) e. _V |
31 |
|
simpr |
|- ( ( B e. V /\ A e. W ) -> A e. W ) |
32 |
|
uniiun |
|- U. z = U_ x e. z x |
33 |
|
eltg3i |
|- ( ( B e. V /\ z C_ B ) -> U. z e. ( topGen ` B ) ) |
34 |
32 33
|
eqeltrrid |
|- ( ( B e. V /\ z C_ B ) -> U_ x e. z x e. ( topGen ` B ) ) |
35 |
34
|
adantlr |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U_ x e. z x e. ( topGen ` B ) ) |
36 |
|
elrestr |
|- ( ( ( topGen ` B ) e. _V /\ A e. W /\ U_ x e. z x e. ( topGen ` B ) ) -> ( U_ x e. z x i^i A ) e. ( ( topGen ` B ) |`t A ) ) |
37 |
30 31 35 36
|
mp3an2ani |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( U_ x e. z x i^i A ) e. ( ( topGen ` B ) |`t A ) ) |
38 |
29 37
|
eqeltrd |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ( ( x e. B |-> ( x i^i A ) ) " z ) e. ( ( topGen ` B ) |`t A ) ) |
39 |
|
unieq |
|- ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> U. y = U. ( ( x e. B |-> ( x i^i A ) ) " z ) ) |
40 |
39
|
eleq1d |
|- ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> ( U. y e. ( ( topGen ` B ) |`t A ) <-> U. ( ( x e. B |-> ( x i^i A ) ) " z ) e. ( ( topGen ` B ) |`t A ) ) ) |
41 |
38 40
|
syl5ibrcom |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( y = ( ( x e. B |-> ( x i^i A ) ) " z ) -> U. y e. ( ( topGen ` B ) |`t A ) ) ) |
42 |
41
|
expimpd |
|- ( ( B e. V /\ A e. W ) -> ( ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) ) |
43 |
42
|
exlimdv |
|- ( ( B e. V /\ A e. W ) -> ( E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) ) |
44 |
43
|
adantr |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> ( E. z ( z C_ B /\ y = ( ( x e. B |-> ( x i^i A ) ) " z ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) ) |
45 |
19 44
|
mpd |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> U. y e. ( ( topGen ` B ) |`t A ) ) |
46 |
|
eleq1 |
|- ( x = U. y -> ( x e. ( ( topGen ` B ) |`t A ) <-> U. y e. ( ( topGen ` B ) |`t A ) ) ) |
47 |
45 46
|
syl5ibrcom |
|- ( ( ( B e. V /\ A e. W ) /\ y C_ ( B |`t A ) ) -> ( x = U. y -> x e. ( ( topGen ` B ) |`t A ) ) ) |
48 |
47
|
expimpd |
|- ( ( B e. V /\ A e. W ) -> ( ( y C_ ( B |`t A ) /\ x = U. y ) -> x e. ( ( topGen ` B ) |`t A ) ) ) |
49 |
48
|
exlimdv |
|- ( ( B e. V /\ A e. W ) -> ( E. y ( y C_ ( B |`t A ) /\ x = U. y ) -> x e. ( ( topGen ` B ) |`t A ) ) ) |
50 |
3 49
|
syl5bi |
|- ( ( B e. V /\ A e. W ) -> ( x e. ( topGen ` ( B |`t A ) ) -> x e. ( ( topGen ` B ) |`t A ) ) ) |
51 |
50
|
ssrdv |
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B |`t A ) ) C_ ( ( topGen ` B ) |`t A ) ) |
52 |
|
restval |
|- ( ( ( topGen ` B ) e. _V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) = ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) ) |
53 |
30 31 52
|
sylancr |
|- ( ( B e. V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) = ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) ) |
54 |
|
eltg3 |
|- ( B e. V -> ( w e. ( topGen ` B ) <-> E. z ( z C_ B /\ w = U. z ) ) ) |
55 |
54
|
adantr |
|- ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) <-> E. z ( z C_ B /\ w = U. z ) ) ) |
56 |
32
|
ineq1i |
|- ( U. z i^i A ) = ( U_ x e. z x i^i A ) |
57 |
56 28
|
eqtr4i |
|- ( U. z i^i A ) = U_ x e. z ( x i^i A ) |
58 |
|
simplll |
|- ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> B e. V ) |
59 |
|
simpllr |
|- ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> A e. W ) |
60 |
|
simpr |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> z C_ B ) |
61 |
60
|
sselda |
|- ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> x e. B ) |
62 |
|
elrestr |
|- ( ( B e. V /\ A e. W /\ x e. B ) -> ( x i^i A ) e. ( B |`t A ) ) |
63 |
58 59 61 62
|
syl3anc |
|- ( ( ( ( B e. V /\ A e. W ) /\ z C_ B ) /\ x e. z ) -> ( x i^i A ) e. ( B |`t A ) ) |
64 |
63
|
fmpttd |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( x e. z |-> ( x i^i A ) ) : z --> ( B |`t A ) ) |
65 |
64
|
frnd |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ran ( x e. z |-> ( x i^i A ) ) C_ ( B |`t A ) ) |
66 |
|
eltg3i |
|- ( ( ( B |`t A ) e. _V /\ ran ( x e. z |-> ( x i^i A ) ) C_ ( B |`t A ) ) -> U. ran ( x e. z |-> ( x i^i A ) ) e. ( topGen ` ( B |`t A ) ) ) |
67 |
1 65 66
|
sylancr |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U. ran ( x e. z |-> ( x i^i A ) ) e. ( topGen ` ( B |`t A ) ) ) |
68 |
26 67
|
eqeltrid |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> U_ x e. z ( x i^i A ) e. ( topGen ` ( B |`t A ) ) ) |
69 |
57 68
|
eqeltrid |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( U. z i^i A ) e. ( topGen ` ( B |`t A ) ) ) |
70 |
|
ineq1 |
|- ( w = U. z -> ( w i^i A ) = ( U. z i^i A ) ) |
71 |
70
|
eleq1d |
|- ( w = U. z -> ( ( w i^i A ) e. ( topGen ` ( B |`t A ) ) <-> ( U. z i^i A ) e. ( topGen ` ( B |`t A ) ) ) ) |
72 |
69 71
|
syl5ibrcom |
|- ( ( ( B e. V /\ A e. W ) /\ z C_ B ) -> ( w = U. z -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) ) |
73 |
72
|
expimpd |
|- ( ( B e. V /\ A e. W ) -> ( ( z C_ B /\ w = U. z ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) ) |
74 |
73
|
exlimdv |
|- ( ( B e. V /\ A e. W ) -> ( E. z ( z C_ B /\ w = U. z ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) ) |
75 |
55 74
|
sylbid |
|- ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) ) |
76 |
75
|
imp |
|- ( ( ( B e. V /\ A e. W ) /\ w e. ( topGen ` B ) ) -> ( w i^i A ) e. ( topGen ` ( B |`t A ) ) ) |
77 |
76
|
fmpttd |
|- ( ( B e. V /\ A e. W ) -> ( w e. ( topGen ` B ) |-> ( w i^i A ) ) : ( topGen ` B ) --> ( topGen ` ( B |`t A ) ) ) |
78 |
77
|
frnd |
|- ( ( B e. V /\ A e. W ) -> ran ( w e. ( topGen ` B ) |-> ( w i^i A ) ) C_ ( topGen ` ( B |`t A ) ) ) |
79 |
53 78
|
eqsstrd |
|- ( ( B e. V /\ A e. W ) -> ( ( topGen ` B ) |`t A ) C_ ( topGen ` ( B |`t A ) ) ) |
80 |
51 79
|
eqssd |
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) ) |