Metamath Proof Explorer

Theorem toponcomb

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

Ref Expression
Assertion toponcomb 
|- ( ( J e. Top /\ K e. Top ) -> ( J e. ( TopOn ` U. K ) <-> K e. ( TopOn ` U. J ) ) )

Proof

Step Hyp Ref Expression
1 toponcom 
 |-  ( ( K e. Top /\ J e. ( TopOn ` U. K ) ) -> K e. ( TopOn ` U. J ) )
2 1 ex 
 |-  ( K e. Top -> ( J e. ( TopOn ` U. K ) -> K e. ( TopOn ` U. J ) ) )
3 2 adantl 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J e. ( TopOn ` U. K ) -> K e. ( TopOn ` U. J ) ) )
4 toponcom 
 |-  ( ( J e. Top /\ K e. ( TopOn ` U. J ) ) -> J e. ( TopOn ` U. K ) )
5 4 ex 
 |-  ( J e. Top -> ( K e. ( TopOn ` U. J ) -> J e. ( TopOn ` U. K ) ) )
6 5 adantr 
 |-  ( ( J e. Top /\ K e. Top ) -> ( K e. ( TopOn ` U. J ) -> J e. ( TopOn ` U. K ) ) )
7 3 6 impbid 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J e. ( TopOn ` U. K ) <-> K e. ( TopOn ` U. J ) ) )