# 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
Assertion fneval

### Proof

Step Hyp Ref Expression
1 fneval.1
2 1 breqi
3 brin ${⊢}{A}\left(\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}\right){B}↔\left({A}\mathrm{Fne}{B}\wedge {A}{\mathrm{Fne}}^{-1}{B}\right)$
4 fnerel ${⊢}\mathrm{Rel}\mathrm{Fne}$
5 4 relbrcnv ${⊢}{A}{\mathrm{Fne}}^{-1}{B}↔{B}\mathrm{Fne}{A}$
6 5 anbi2i ${⊢}\left({A}\mathrm{Fne}{B}\wedge {A}{\mathrm{Fne}}^{-1}{B}\right)↔\left({A}\mathrm{Fne}{B}\wedge {B}\mathrm{Fne}{A}\right)$
7 3 6 bitri ${⊢}{A}\left(\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}\right){B}↔\left({A}\mathrm{Fne}{B}\wedge {B}\mathrm{Fne}{A}\right)$
8 2 7 bitri
9 eqid ${⊢}\bigcup {A}=\bigcup {A}$
10 eqid ${⊢}\bigcup {B}=\bigcup {B}$
11 9 10 isfne4b ${⊢}{B}\in {W}\to \left({A}\mathrm{Fne}{B}↔\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\right)\right)$
12 10 9 isfne4b ${⊢}{A}\in {V}\to \left({B}\mathrm{Fne}{A}↔\left(\bigcup {B}=\bigcup {A}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)$
13 eqcom ${⊢}\bigcup {B}=\bigcup {A}↔\bigcup {A}=\bigcup {B}$
14 13 anbi1i ${⊢}\left(\bigcup {B}=\bigcup {A}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)↔\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)$
15 12 14 syl6bb ${⊢}{A}\in {V}\to \left({B}\mathrm{Fne}{A}↔\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)$
16 11 15 bi2anan9r ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\mathrm{Fne}{B}\wedge {B}\mathrm{Fne}{A}\right)↔\left(\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)\right)$
17 eqss ${⊢}\mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)↔\left(\mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)$
18 17 anbi2i ${⊢}\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\right)↔\left(\bigcup {A}=\bigcup {B}\wedge \left(\mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)$
19 anandi ${⊢}\left(\bigcup {A}=\bigcup {B}\wedge \left(\mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)↔\left(\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)$
20 18 19 bitri ${⊢}\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\right)↔\left(\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({B}\right)\subseteq \mathrm{topGen}\left({A}\right)\right)\right)$
21 16 20 bitr4di ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\mathrm{Fne}{B}\wedge {B}\mathrm{Fne}{A}\right)↔\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\right)\right)$
22 unieq ${⊢}\mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\to \bigcup \mathrm{topGen}\left({A}\right)=\bigcup \mathrm{topGen}\left({B}\right)$
23 unitg ${⊢}{A}\in {V}\to \bigcup \mathrm{topGen}\left({A}\right)=\bigcup {A}$
24 unitg ${⊢}{B}\in {W}\to \bigcup \mathrm{topGen}\left({B}\right)=\bigcup {B}$
25 23 24 eqeqan12d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\bigcup \mathrm{topGen}\left({A}\right)=\bigcup \mathrm{topGen}\left({B}\right)↔\bigcup {A}=\bigcup {B}\right)$
26 22 25 syl5ib ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\to \bigcup {A}=\bigcup {B}\right)$
27 26 pm4.71rd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)↔\left(\bigcup {A}=\bigcup {B}\wedge \mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\right)\right)$
28 21 27 bitr4d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\mathrm{Fne}{B}\wedge {B}\mathrm{Fne}{A}\right)↔\mathrm{topGen}\left({A}\right)=\mathrm{topGen}\left({B}\right)\right)$
29 8 28 syl5bb