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	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
Assertion	fneval	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\underset{\dot{}}{\sim }B\leftrightarrow \mathrm{topGen}\left(A\right)=\mathrm{topGen}\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fneval.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
2	1	breqi	$$⊢A\underset{\dot{}}{\sim }B\leftrightarrow A\left(\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}\right)B$$
3		brin	$$⊢A\left(\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}\right)B\leftrightarrow \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\leftrightarrow B\mathrm{Fne}A$$
6	5	anbi2i	$$⊢\left(A\mathrm{Fne}B\wedge A{\mathrm{Fne}}^{-1}B\right)\leftrightarrow \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\leftrightarrow \left(A\mathrm{Fne}B\wedge B\mathrm{Fne}A\right)$$
8	2 7	bitri	$$⊢A\underset{\dot{}}{\sim }B\leftrightarrow \left(A\mathrm{Fne}B\wedge B\mathrm{Fne}A\right)$$
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\leftrightarrow \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\leftrightarrow \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\leftrightarrow \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)\leftrightarrow \left(\bigcup A=\bigcup B\wedge \mathrm{topGen}\left(B\right)\subseteq \mathrm{topGen}\left(A\right)\right)$$
15	12 14	bitrdi	$$⊢A\in V\to \left(B\mathrm{Fne}A\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \bigcup A=\bigcup B\right)$$
26	22 25	imbitrid	$$⊢\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)\leftrightarrow \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)\leftrightarrow \mathrm{topGen}\left(A\right)=\mathrm{topGen}\left(B\right)\right)$$
29	8 28	bitrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\underset{\dot{}}{\sim }B\leftrightarrow \mathrm{topGen}\left(A\right)=\mathrm{topGen}\left(B\right)\right)$$