# Metamath Proof Explorer

## Theorem hmphtr

Description: "Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmphtr
|- ( ( J ~= K /\ K ~= L ) -> J ~= L )

### Proof

Step Hyp Ref Expression
1 hmph
|-  ( J ~= K <-> ( J Homeo K ) =/= (/) )
2 hmph
|-  ( K ~= L <-> ( K Homeo L ) =/= (/) )
3 n0
|-  ( ( J Homeo K ) =/= (/) <-> E. f f e. ( J Homeo K ) )
4 n0
|-  ( ( K Homeo L ) =/= (/) <-> E. g g e. ( K Homeo L ) )
5 exdistrv
|-  ( E. f E. g ( f e. ( J Homeo K ) /\ g e. ( K Homeo L ) ) <-> ( E. f f e. ( J Homeo K ) /\ E. g g e. ( K Homeo L ) ) )
6 hmeoco
|-  ( ( f e. ( J Homeo K ) /\ g e. ( K Homeo L ) ) -> ( g o. f ) e. ( J Homeo L ) )
7 hmphi
|-  ( ( g o. f ) e. ( J Homeo L ) -> J ~= L )
8 6 7 syl
|-  ( ( f e. ( J Homeo K ) /\ g e. ( K Homeo L ) ) -> J ~= L )
9 8 exlimivv
|-  ( E. f E. g ( f e. ( J Homeo K ) /\ g e. ( K Homeo L ) ) -> J ~= L )
10 5 9 sylbir
|-  ( ( E. f f e. ( J Homeo K ) /\ E. g g e. ( K Homeo L ) ) -> J ~= L )
11 3 4 10 syl2anb
|-  ( ( ( J Homeo K ) =/= (/) /\ ( K Homeo L ) =/= (/) ) -> J ~= L )
12 1 2 11 syl2anb
|-  ( ( J ~= K /\ K ~= L ) -> J ~= L )