Metamath Proof Explorer


Theorem fzo0

Description: Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzo0 ( 𝐴 ..^ 𝐴 ) = ∅

Proof

Step Hyp Ref Expression
1 fzonel ¬ 𝐴 ∈ ( 𝐴 ..^ 𝐴 )
2 fzon0 ( ( 𝐴 ..^ 𝐴 ) ≠ ∅ ↔ 𝐴 ∈ ( 𝐴 ..^ 𝐴 ) )
3 2 necon1bbii ( ¬ 𝐴 ∈ ( 𝐴 ..^ 𝐴 ) ↔ ( 𝐴 ..^ 𝐴 ) = ∅ )
4 1 3 mpbi ( 𝐴 ..^ 𝐴 ) = ∅