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 Fne -1
Assertion fneval A V B W A ˙ B topGen A = topGen B

Proof

Step Hyp Ref Expression
1 fneval.1 ˙ = Fne Fne -1
2 1 breqi A ˙ B A Fne Fne -1 B
3 brin A Fne Fne -1 B A Fne B A Fne -1 B
4 fnerel Rel Fne
5 4 relbrcnv A Fne -1 B B Fne A
6 5 anbi2i A Fne B A Fne -1 B A Fne B B Fne A
7 3 6 bitri A Fne Fne -1 B A Fne B B Fne A
8 2 7 bitri A ˙ B A Fne B B Fne A
9 eqid A = A
10 eqid B = B
11 9 10 isfne4b B W A Fne B A = B topGen A topGen B
12 10 9 isfne4b A V B Fne A B = A topGen B topGen A
13 eqcom B = A A = B
14 13 anbi1i B = A topGen B topGen A A = B topGen B topGen A
15 12 14 bitrdi A V B Fne A A = B topGen B topGen A
16 11 15 bi2anan9r A V B W A Fne B B Fne A A = B topGen A topGen B A = B topGen B topGen A
17 eqss topGen A = topGen B topGen A topGen B topGen B topGen A
18 17 anbi2i A = B topGen A = topGen B A = B topGen A topGen B topGen B topGen A
19 anandi A = B topGen A topGen B topGen B topGen A A = B topGen A topGen B A = B topGen B topGen A
20 18 19 bitri A = B topGen A = topGen B A = B topGen A topGen B A = B topGen B topGen A
21 16 20 bitr4di A V B W A Fne B B Fne A A = B topGen A = topGen B
22 unieq topGen A = topGen B topGen A = topGen B
23 unitg A V topGen A = A
24 unitg B W topGen B = B
25 23 24 eqeqan12d A V B W topGen A = topGen B A = B
26 22 25 syl5ib A V B W topGen A = topGen B A = B
27 26 pm4.71rd A V B W topGen A = topGen B A = B topGen A = topGen B
28 21 27 bitr4d A V B W A Fne B B Fne A topGen A = topGen B
29 8 28 syl5bb A V B W A ˙ B topGen A = topGen B