Theorem topfne

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

	Ref	Expression
Hypotheses	topfne.1	⊢ 𝑋 = ∪ 𝐽
	topfne.2	⊢ 𝑌 = ∪ 𝐾
Assertion	topfne	⊢ ( ( 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) → ( 𝐽 ⊆ 𝐾 ↔ 𝐽 Fne 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		topfne.1	⊢ 𝑋 = ∪ 𝐽
2		topfne.2	⊢ 𝑌 = ∪ 𝐾
3		tgtop	⊢ ( 𝐾 ∈ Top → ( topGen ‘ 𝐾 ) = 𝐾 )
4	3	sseq2d	⊢ ( 𝐾 ∈ Top → ( 𝐽 ⊆ ( topGen ‘ 𝐾 ) ↔ 𝐽 ⊆ 𝐾 ) )
5	4	bicomd	⊢ ( 𝐾 ∈ Top → ( 𝐽 ⊆ 𝐾 ↔ 𝐽 ⊆ ( topGen ‘ 𝐾 ) ) )
6	1 2	isfne4	⊢ ( 𝐽 Fne 𝐾 ↔ ( 𝑋 = 𝑌 ∧ 𝐽 ⊆ ( topGen ‘ 𝐾 ) ) )
7	6	baibr	⊢ ( 𝑋 = 𝑌 → ( 𝐽 ⊆ ( topGen ‘ 𝐾 ) ↔ 𝐽 Fne 𝐾 ) )
8	5 7	sylan9bb	⊢ ( ( 𝐾 ∈ Top ∧ 𝑋 = 𝑌 ) → ( 𝐽 ⊆ 𝐾 ↔ 𝐽 Fne 𝐾 ) )