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 J Comp J Top y 𝒫 J X = y z 𝒫 y Fin X = z

Proof

Step Hyp Ref Expression
1 iscmp.1 X = J
2 pweq x = J 𝒫 x = 𝒫 J
3 unieq x = J x = J
4 3 1 syl6eqr x = J x = X
5 4 eqeq1d x = J x = y X = y
6 4 eqeq1d x = J x = z X = z
7 6 rexbidv x = J z 𝒫 y Fin x = z z 𝒫 y Fin X = z
8 5 7 imbi12d x = J x = y z 𝒫 y Fin x = z X = y z 𝒫 y Fin X = z
9 2 8 raleqbidv x = J y 𝒫 x x = y z 𝒫 y Fin x = z y 𝒫 J X = y z 𝒫 y Fin X = z
10 df-cmp Comp = x Top | y 𝒫 x x = y z 𝒫 y Fin x = z
11 9 10 elrab2 J Comp J Top y 𝒫 J X = y z 𝒫 y Fin X = z