Metamath Proof Explorer

Theorem fneval

Description: Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis fneval.1 
|- .~ = ( Fne i^i `' Fne )
Assertion fneval 
|- ( ( A e. V /\ B e. W ) -> ( A .~ B <-> ( topGen ` A ) = ( topGen ` B ) ) )

Proof

Step Hyp Ref Expression
1 fneval.1 
 |-  .~ = ( Fne i^i `' Fne )
2 1 breqi 
 |-  ( A .~ B <-> A ( Fne i^i `' Fne ) B )
3 brin 
 |-  ( A ( Fne i^i `' Fne ) B <-> ( A Fne B /\ A `' Fne B ) )
4 fnerel 
 |-  Rel Fne
5 4 relbrcnv 
 |-  ( A `' Fne B <-> B Fne A )
6 5 anbi2i 
 |-  ( ( A Fne B /\ A `' Fne B ) <-> ( A Fne B /\ B Fne A ) )
7 3 6 bitri 
 |-  ( A ( Fne i^i `' Fne ) B <-> ( A Fne B /\ B Fne A ) )
8 2 7 bitri 
 |-  ( A .~ B <-> ( A Fne B /\ B Fne A ) )
9 eqid 
 |-  U. A = U. A
10 eqid 
 |-  U. B = U. B
11 9 10 isfne4b 
 |-  ( B e. W -> ( A Fne B <-> ( U. A = U. B /\ ( topGen ` A ) C_ ( topGen ` B ) ) ) )
12 10 9 isfne4b 
 |-  ( A e. V -> ( B Fne A <-> ( U. B = U. A /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) )
13 eqcom 
 |-  ( U. B = U. A <-> U. A = U. B )
14 13 anbi1i 
 |-  ( ( U. B = U. A /\ ( topGen ` B ) C_ ( topGen ` A ) ) <-> ( U. A = U. B /\ ( topGen ` B ) C_ ( topGen ` A ) ) )
15 12 14 bitrdi 
 |-  ( A e. V -> ( B Fne A <-> ( U. A = U. B /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) )
16 11 15 bi2anan9r 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A Fne B /\ B Fne A ) <-> ( ( U. A = U. B /\ ( topGen ` A ) C_ ( topGen ` B ) ) /\ ( U. A = U. B /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) ) )
17 eqss 
 |-  ( ( topGen ` A ) = ( topGen ` B ) <-> ( ( topGen ` A ) C_ ( topGen ` B ) /\ ( topGen ` B ) C_ ( topGen ` A ) ) )
18 17 anbi2i 
 |-  ( ( U. A = U. B /\ ( topGen ` A ) = ( topGen ` B ) ) <-> ( U. A = U. B /\ ( ( topGen ` A ) C_ ( topGen ` B ) /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) )
19 anandi 
 |-  ( ( U. A = U. B /\ ( ( topGen ` A ) C_ ( topGen ` B ) /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) <-> ( ( U. A = U. B /\ ( topGen ` A ) C_ ( topGen ` B ) ) /\ ( U. A = U. B /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) )
20 18 19 bitri 
 |-  ( ( U. A = U. B /\ ( topGen ` A ) = ( topGen ` B ) ) <-> ( ( U. A = U. B /\ ( topGen ` A ) C_ ( topGen ` B ) ) /\ ( U. A = U. B /\ ( topGen ` B ) C_ ( topGen ` A ) ) ) )
21 16 20 bitr4di 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A Fne B /\ B Fne A ) <-> ( U. A = U. B /\ ( topGen ` A ) = ( topGen ` B ) ) ) )
22 unieq 
 |-  ( ( topGen ` A ) = ( topGen ` B ) -> U. ( topGen ` A ) = U. ( topGen ` B ) )
23 unitg 
 |-  ( A e. V -> U. ( topGen ` A ) = U. A )
24 unitg 
 |-  ( B e. W -> U. ( topGen ` B ) = U. B )
25 23 24 eqeqan12d 
 |-  ( ( A e. V /\ B e. W ) -> ( U. ( topGen ` A ) = U. ( topGen ` B ) <-> U. A = U. B ) )
26 22 25 imbitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( ( topGen ` A ) = ( topGen ` B ) -> U. A = U. B ) )
27 26 pm4.71rd 
 |-  ( ( A e. V /\ B e. W ) -> ( ( topGen ` A ) = ( topGen ` B ) <-> ( U. A = U. B /\ ( topGen ` A ) = ( topGen ` B ) ) ) )
28 21 27 bitr4d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A Fne B /\ B Fne A ) <-> ( topGen ` A ) = ( topGen ` B ) ) )
29 8 28 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( A .~ B <-> ( topGen ` A ) = ( topGen ` B ) ) )