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 ‘ ∪ 𝐽 ) ) )