Metamath Proof Explorer

Theorem toponcomb

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

Ref Expression
Assertion toponcomb ⊢ J ∈ Top ∧ K ∈ Top → J ∈ TopOn ⁡ ⋃ K ↔ K ∈ TopOn ⁡ ⋃ J

Proof

Step Hyp Ref Expression
1 toponcom ⊢ K ∈ Top ∧ J ∈ TopOn ⁡ ⋃ K → K ∈ TopOn ⁡ ⋃ J
2 1 ex ⊢ K ∈ Top → J ∈ TopOn ⁡ ⋃ K → K ∈ TopOn ⁡ ⋃ J
3 2 adantl ⊢ J ∈ Top ∧ K ∈ Top → J ∈ TopOn ⁡ ⋃ K → K ∈ TopOn ⁡ ⋃ J
4 toponcom ⊢ J ∈ Top ∧ K ∈ TopOn ⁡ ⋃ J → J ∈ TopOn ⁡ ⋃ K
5 4 ex ⊢ J ∈ Top → K ∈ TopOn ⁡ ⋃ J → J ∈ TopOn ⁡ ⋃ K
6 5 adantr ⊢ J ∈ Top ∧ K ∈ Top → K ∈ TopOn ⁡ ⋃ J → J ∈ TopOn ⁡ ⋃ K
7 3 6 impbid ⊢ J ∈ Top ∧ K ∈ Top → J ∈ TopOn ⁡ ⋃ K ↔ K ∈ TopOn ⁡ ⋃ J