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 123N=

Proof

Step Hyp Ref Expression
1 2lt3 2<3
2 fzdisj 2<3123N=
3 1 2 ax-mp 123N=