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