Step |
Hyp |
Ref |
Expression |
1 |
|
elrest |
|- ( ( B e. TopBases /\ A e. _V ) -> ( a e. ( B |`t A ) <-> E. u e. B a = ( u i^i A ) ) ) |
2 |
|
elrest |
|- ( ( B e. TopBases /\ A e. _V ) -> ( b e. ( B |`t A ) <-> E. v e. B b = ( v i^i A ) ) ) |
3 |
1 2
|
anbi12d |
|- ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) <-> ( E. u e. B a = ( u i^i A ) /\ E. v e. B b = ( v i^i A ) ) ) ) |
4 |
|
reeanv |
|- ( E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) <-> ( E. u e. B a = ( u i^i A ) /\ E. v e. B b = ( v i^i A ) ) ) |
5 |
3 4
|
bitr4di |
|- ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) <-> E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) ) ) |
6 |
|
simplll |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> B e. TopBases ) |
7 |
|
simplrl |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> u e. B ) |
8 |
|
simplrr |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> v e. B ) |
9 |
|
simpr |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> c e. ( ( u i^i v ) i^i A ) ) |
10 |
9
|
elin1d |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> c e. ( u i^i v ) ) |
11 |
|
basis2 |
|- ( ( ( B e. TopBases /\ u e. B ) /\ ( v e. B /\ c e. ( u i^i v ) ) ) -> E. z e. B ( c e. z /\ z C_ ( u i^i v ) ) ) |
12 |
6 7 8 10 11
|
syl22anc |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> E. z e. B ( c e. z /\ z C_ ( u i^i v ) ) ) |
13 |
|
simplll |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( B e. TopBases /\ A e. _V ) ) |
14 |
13
|
simpld |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> B e. TopBases ) |
15 |
13
|
simprd |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> A e. _V ) |
16 |
|
simprl |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> z e. B ) |
17 |
|
elrestr |
|- ( ( B e. TopBases /\ A e. _V /\ z e. B ) -> ( z i^i A ) e. ( B |`t A ) ) |
18 |
14 15 16 17
|
syl3anc |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( z i^i A ) e. ( B |`t A ) ) |
19 |
|
simprrl |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. z ) |
20 |
|
simplr |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. ( ( u i^i v ) i^i A ) ) |
21 |
20
|
elin2d |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. A ) |
22 |
19 21
|
elind |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> c e. ( z i^i A ) ) |
23 |
|
simprrr |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> z C_ ( u i^i v ) ) |
24 |
23
|
ssrind |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) |
25 |
|
eleq2 |
|- ( w = ( z i^i A ) -> ( c e. w <-> c e. ( z i^i A ) ) ) |
26 |
|
sseq1 |
|- ( w = ( z i^i A ) -> ( w C_ ( ( u i^i v ) i^i A ) <-> ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) ) |
27 |
25 26
|
anbi12d |
|- ( w = ( z i^i A ) -> ( ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) <-> ( c e. ( z i^i A ) /\ ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) ) ) |
28 |
27
|
rspcev |
|- ( ( ( z i^i A ) e. ( B |`t A ) /\ ( c e. ( z i^i A ) /\ ( z i^i A ) C_ ( ( u i^i v ) i^i A ) ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) |
29 |
18 22 24 28
|
syl12anc |
|- ( ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) /\ ( z e. B /\ ( c e. z /\ z C_ ( u i^i v ) ) ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) |
30 |
12 29
|
rexlimddv |
|- ( ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) /\ c e. ( ( u i^i v ) i^i A ) ) -> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) |
31 |
30
|
ralrimiva |
|- ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) -> A. c e. ( ( u i^i v ) i^i A ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) |
32 |
|
ineq12 |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( a i^i b ) = ( ( u i^i A ) i^i ( v i^i A ) ) ) |
33 |
|
inindir |
|- ( ( u i^i v ) i^i A ) = ( ( u i^i A ) i^i ( v i^i A ) ) |
34 |
32 33
|
eqtr4di |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( a i^i b ) = ( ( u i^i v ) i^i A ) ) |
35 |
34
|
sseq2d |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( w C_ ( a i^i b ) <-> w C_ ( ( u i^i v ) i^i A ) ) ) |
36 |
35
|
anbi2d |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( ( c e. w /\ w C_ ( a i^i b ) ) <-> ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) ) |
37 |
36
|
rexbidv |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) <-> E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) ) |
38 |
34 37
|
raleqbidv |
|- ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> ( A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) <-> A. c e. ( ( u i^i v ) i^i A ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( ( u i^i v ) i^i A ) ) ) ) |
39 |
31 38
|
syl5ibrcom |
|- ( ( ( B e. TopBases /\ A e. _V ) /\ ( u e. B /\ v e. B ) ) -> ( ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) ) |
40 |
39
|
rexlimdvva |
|- ( ( B e. TopBases /\ A e. _V ) -> ( E. u e. B E. v e. B ( a = ( u i^i A ) /\ b = ( v i^i A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) ) |
41 |
5 40
|
sylbid |
|- ( ( B e. TopBases /\ A e. _V ) -> ( ( a e. ( B |`t A ) /\ b e. ( B |`t A ) ) -> A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) ) |
42 |
41
|
ralrimivv |
|- ( ( B e. TopBases /\ A e. _V ) -> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) |
43 |
|
ovex |
|- ( B |`t A ) e. _V |
44 |
|
isbasis2g |
|- ( ( B |`t A ) e. _V -> ( ( B |`t A ) e. TopBases <-> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) ) |
45 |
43 44
|
ax-mp |
|- ( ( B |`t A ) e. TopBases <-> A. a e. ( B |`t A ) A. b e. ( B |`t A ) A. c e. ( a i^i b ) E. w e. ( B |`t A ) ( c e. w /\ w C_ ( a i^i b ) ) ) |
46 |
42 45
|
sylibr |
|- ( ( B e. TopBases /\ A e. _V ) -> ( B |`t A ) e. TopBases ) |
47 |
|
relxp |
|- Rel ( _V X. _V ) |
48 |
|
restfn |
|- |`t Fn ( _V X. _V ) |
49 |
|
fndm |
|- ( |`t Fn ( _V X. _V ) -> dom |`t = ( _V X. _V ) ) |
50 |
48 49
|
ax-mp |
|- dom |`t = ( _V X. _V ) |
51 |
50
|
releqi |
|- ( Rel dom |`t <-> Rel ( _V X. _V ) ) |
52 |
47 51
|
mpbir |
|- Rel dom |`t |
53 |
52
|
ovprc2 |
|- ( -. A e. _V -> ( B |`t A ) = (/) ) |
54 |
53
|
adantl |
|- ( ( B e. TopBases /\ -. A e. _V ) -> ( B |`t A ) = (/) ) |
55 |
|
fi0 |
|- ( fi ` (/) ) = (/) |
56 |
|
fibas |
|- ( fi ` (/) ) e. TopBases |
57 |
55 56
|
eqeltrri |
|- (/) e. TopBases |
58 |
54 57
|
eqeltrdi |
|- ( ( B e. TopBases /\ -. A e. _V ) -> ( B |`t A ) e. TopBases ) |
59 |
46 58
|
pm2.61dan |
|- ( B e. TopBases -> ( B |`t A ) e. TopBases ) |