Step |
Hyp |
Ref |
Expression |
1 |
|
topfneec.1 |
|- .~ = ( Fne i^i `' Fne ) |
2 |
1
|
fneer |
|- .~ Er _V |
3 |
|
errel |
|- ( .~ Er _V -> Rel .~ ) |
4 |
2 3
|
ax-mp |
|- Rel .~ |
5 |
|
relelec |
|- ( Rel .~ -> ( A e. [ J ] .~ <-> J .~ A ) ) |
6 |
4 5
|
ax-mp |
|- ( A e. [ J ] .~ <-> J .~ A ) |
7 |
4
|
brrelex2i |
|- ( J .~ A -> A e. _V ) |
8 |
7
|
a1i |
|- ( J e. Top -> ( J .~ A -> A e. _V ) ) |
9 |
|
eleq1 |
|- ( ( topGen ` A ) = J -> ( ( topGen ` A ) e. Top <-> J e. Top ) ) |
10 |
9
|
biimparc |
|- ( ( J e. Top /\ ( topGen ` A ) = J ) -> ( topGen ` A ) e. Top ) |
11 |
|
tgclb |
|- ( A e. TopBases <-> ( topGen ` A ) e. Top ) |
12 |
10 11
|
sylibr |
|- ( ( J e. Top /\ ( topGen ` A ) = J ) -> A e. TopBases ) |
13 |
|
elex |
|- ( A e. TopBases -> A e. _V ) |
14 |
12 13
|
syl |
|- ( ( J e. Top /\ ( topGen ` A ) = J ) -> A e. _V ) |
15 |
14
|
ex |
|- ( J e. Top -> ( ( topGen ` A ) = J -> A e. _V ) ) |
16 |
1
|
fneval |
|- ( ( J e. Top /\ A e. _V ) -> ( J .~ A <-> ( topGen ` J ) = ( topGen ` A ) ) ) |
17 |
|
tgtop |
|- ( J e. Top -> ( topGen ` J ) = J ) |
18 |
17
|
eqeq1d |
|- ( J e. Top -> ( ( topGen ` J ) = ( topGen ` A ) <-> J = ( topGen ` A ) ) ) |
19 |
|
eqcom |
|- ( J = ( topGen ` A ) <-> ( topGen ` A ) = J ) |
20 |
18 19
|
syl6bb |
|- ( J e. Top -> ( ( topGen ` J ) = ( topGen ` A ) <-> ( topGen ` A ) = J ) ) |
21 |
20
|
adantr |
|- ( ( J e. Top /\ A e. _V ) -> ( ( topGen ` J ) = ( topGen ` A ) <-> ( topGen ` A ) = J ) ) |
22 |
16 21
|
bitrd |
|- ( ( J e. Top /\ A e. _V ) -> ( J .~ A <-> ( topGen ` A ) = J ) ) |
23 |
22
|
ex |
|- ( J e. Top -> ( A e. _V -> ( J .~ A <-> ( topGen ` A ) = J ) ) ) |
24 |
8 15 23
|
pm5.21ndd |
|- ( J e. Top -> ( J .~ A <-> ( topGen ` A ) = J ) ) |
25 |
6 24
|
syl5bb |
|- ( J e. Top -> ( A e. [ J ] .~ <-> ( topGen ` A ) = J ) ) |