This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toponcomb

Description: Biconditional form of toponcom . (Contributed by BJ, 5-Dec-2021)

Ref Expression
Assertion toponcomb ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 toponcom ⊢ ( ( 𝐾 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2 1 ex ⊢ ( 𝐾 ∈ Top → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )
3 2 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )
4 toponcom ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) )
5 4 ex ⊢ ( 𝐽 ∈ Top → ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) )
6 5 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ) )
7 3 6 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐾 ) ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐽 ) ) )