Theorem fnetg

Description: A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Assertion	fnetg	⊢ ( 𝐴 Fne 𝐵 → 𝐴 ⊆ ( topGen ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐴 = ∪ 𝐴
2		eqid	⊢ ∪ 𝐵 = ∪ 𝐵
3	1 2	isfne4	⊢ ( 𝐴 Fne 𝐵 ↔ ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( topGen ‘ 𝐵 ) ) )
4	3	simprbi	⊢ ( 𝐴 Fne 𝐵 → 𝐴 ⊆ ( topGen ‘ 𝐵 ) )