Metamath Proof Explorer


Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis iscmp.1 X=J
Assertion iscmp JCompJTopy𝒫JX=yz𝒫yFinX=z

Proof

Step Hyp Ref Expression
1 iscmp.1 X=J
2 pweq x=J𝒫x=𝒫J
3 unieq x=Jx=J
4 3 1 eqtr4di x=Jx=X
5 4 eqeq1d x=Jx=yX=y
6 4 eqeq1d x=Jx=zX=z
7 6 rexbidv x=Jz𝒫yFinx=zz𝒫yFinX=z
8 5 7 imbi12d x=Jx=yz𝒫yFinx=zX=yz𝒫yFinX=z
9 2 8 raleqbidv x=Jy𝒫xx=yz𝒫yFinx=zy𝒫JX=yz𝒫yFinX=z
10 df-cmp Comp=xTop|y𝒫xx=yz𝒫yFinx=z
11 9 10 elrab2 JCompJTopy𝒫JX=yz𝒫yFinX=z