Metamath Proof Explorer


Theorem ch0lei

Description: The closed subspace zero is the smallest member of CH . (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1 𝐴C
Assertion ch0lei 0𝐴

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 ch0le ( 𝐴C → 0𝐴 )
3 1 2 ax-mp 0𝐴