Metamath Proof Explorer
Description: Lemma for axlowdim . Show that two sets are disjoint. (Contributed by Scott Fenton, 29-Jun-2013)
|
|
Ref |
Expression |
|
Assertion |
axlowdimlem2 |
⊢ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
2lt3 |
⊢ 2 < 3 |
2 |
|
fzdisj |
⊢ ( 2 < 3 → ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ) |
3 |
1 2
|
ax-mp |
⊢ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ |