Description: A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | ustne0 | ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ≠ ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ustbasel | ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ 𝑈 ) | |
2 | 1 | ne0d | ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ≠ ∅ ) |