Step 
Hyp 
Ref 
Expression 
1 

hmphdis.1 
 X = U. J 
2 

pwuni 
 J C_ ~P U. J 
3 
1

pweqi 
 ~P X = ~P U. J 
4 
2 3

sseqtrri 
 J C_ ~P X 
5 
4

a1i 
 ( J ~= ~P A > J C_ ~P X ) 
6 

hmph 
 ( J ~= ~P A <> ( J Homeo ~P A ) =/= (/) ) 
7 

n0 
 ( ( J Homeo ~P A ) =/= (/) <> E. f f e. ( J Homeo ~P A ) ) 
8 

elpwi 
 ( x e. ~P X > x C_ X ) 
9 

imassrn 
 ( f " x ) C_ ran f 
10 

unipw 
 U. ~P A = A 
11 
10

eqcomi 
 A = U. ~P A 
12 
1 11

hmeof1o 
 ( f e. ( J Homeo ~P A ) > f : X 11onto> A ) 
13 

f1of 
 ( f : X 11onto> A > f : X > A ) 
14 

frn 
 ( f : X > A > ran f C_ A ) 
15 
12 13 14

3syl 
 ( f e. ( J Homeo ~P A ) > ran f C_ A ) 
16 
15

adantr 
 ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) > ran f C_ A ) 
17 
9 16

sstrid 
 ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) > ( f " x ) C_ A ) 
18 

vex 
 f e. _V 
19 
18

imaex 
 ( f " x ) e. _V 
20 
19

elpw 
 ( ( f " x ) e. ~P A <> ( f " x ) C_ A ) 
21 
17 20

sylibr 
 ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) > ( f " x ) e. ~P A ) 
22 
1

hmeoopn 
 ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) > ( x e. J <> ( f " x ) e. ~P A ) ) 
23 
21 22

mpbird 
 ( ( f e. ( J Homeo ~P A ) /\ x C_ X ) > x e. J ) 
24 
23

ex 
 ( f e. ( J Homeo ~P A ) > ( x C_ X > x e. J ) ) 
25 
8 24

syl5 
 ( f e. ( J Homeo ~P A ) > ( x e. ~P X > x e. J ) ) 
26 
25

ssrdv 
 ( f e. ( J Homeo ~P A ) > ~P X C_ J ) 
27 
26

exlimiv 
 ( E. f f e. ( J Homeo ~P A ) > ~P X C_ J ) 
28 
7 27

sylbi 
 ( ( J Homeo ~P A ) =/= (/) > ~P X C_ J ) 
29 
6 28

sylbi 
 ( J ~= ~P A > ~P X C_ J ) 
30 
5 29

eqssd 
 ( J ~= ~P A > J = ~P X ) 