toponcomb

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

		Ref	Expression
	Assertion	toponcomb	$⊢ (J \in Top \land K \in Top) \to (J \in TopOn (⋃ K) \leftrightarrow K \in TopOn (⋃ J))$

Step	Hyp	Ref	Expression
1		toponcom	$⊢ (K \in Top \land J \in TopOn (⋃ K)) \to K \in TopOn (⋃ J)$
2	1	ex	$⊢ K \in Top \to (J \in TopOn (⋃ K) \to K \in TopOn (⋃ J))$
3	2	adantl	$⊢ (J \in Top \land K \in Top) \to (J \in TopOn (⋃ K) \to K \in TopOn (⋃ J))$
4		toponcom	$⊢ (J \in Top \land K \in TopOn (⋃ J)) \to J \in TopOn (⋃ K)$
5	4	ex	$⊢ J \in Top \to (K \in TopOn (⋃ J) \to J \in TopOn (⋃ K))$
6	5	adantr	$⊢ (J \in Top \land K \in Top) \to (K \in TopOn (⋃ J) \to J \in TopOn (⋃ K))$
7	3 6	impbid	$⊢ (J \in Top \land K \in Top) \to (J \in TopOn (⋃ K) \leftrightarrow K \in TopOn (⋃ J))$

Metamath Proof Explorer