Theorem topfne

Description: Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009)

	Ref	Expression
Hypotheses	topfne.1	|- X = U. J
	topfne.2	|- Y = U. K
Assertion	topfne	|- ( ( K e. Top /\ X = Y ) -> ( J C_ K <-> J Fne K ) )

Proof

Step	Hyp	Ref	Expression
1		topfne.1	|- X = U. J
2		topfne.2	|- Y = U. K
3		tgtop	|- ( K e. Top -> ( topGen ` K ) = K )
4	3	sseq2d	|- ( K e. Top -> ( J C_ ( topGen ` K ) <-> J C_ K ) )
5	4	bicomd	|- ( K e. Top -> ( J C_ K <-> J C_ ( topGen ` K ) ) )
6	1 2	isfne4	|- ( J Fne K <-> ( X = Y /\ J C_ ( topGen ` K ) ) )
7	6	baibr	|- ( X = Y -> ( J C_ ( topGen ` K ) <-> J Fne K ) )
8	5 7	sylan9bb	|- ( ( K e. Top /\ X = Y ) -> ( J C_ K <-> J Fne K ) )