Metamath Proof Explorer


Theorem axlowdimlem2

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 ... 𝑁 ) ) = ∅