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 ) i^i ( 3 ... N ) ) = (/)

Proof

Step Hyp Ref Expression
1 2lt3 
 |-  2 < 3
2 fzdisj 
 |-  ( 2 < 3 -> ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/) )
3 1 2 ax-mp 
 |-  ( ( 1 ... 2 ) i^i ( 3 ... N ) ) = (/)