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 )