Theorem toponcom

Description: If K is a topology on the base set of topology J , then J is a topology on the base of K . (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	toponcom	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → ∪ 𝐽 = ∪ 𝐾 )
2	1	eqcomd	⊢ ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → ∪ 𝐾 = ∪ 𝐽 )
3	2	anim2i	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) → ( 𝐽 ∈ Top ∧ ∪ 𝐾 = ∪ 𝐽 ) )
4		istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ↔ ( 𝐽 ∈ Top ∧ ∪ 𝐾 = ∪ 𝐽 ) )
5	3 4	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) )