Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdimlem10 Structured version   Visualization version   Unicode version

Theorem axlowdimlem10 25060
 Description: Lemma for axlowdim 25070. Set up a family of points in Euclidean space. (Contributed by Scott Fenton, 21-Apr-2013.)
Hypothesis
Ref Expression
axlowdimlem10.1
Assertion
Ref Expression
axlowdimlem10

Proof of Theorem axlowdimlem10
StepHypRef Expression
1 ovex 6336 . . . . . . . . 9
2 1ex 9656 . . . . . . . . 9
31, 2f1osn 5866 . . . . . . . 8
4 f1of 5828 . . . . . . . 8
53, 4ax-mp 5 . . . . . . 7
6 c0ex 9655 . . . . . . . 8
76fconst 5782 . . . . . . 7
85, 7pm3.2i 462 . . . . . 6
9 disjdif 3830 . . . . . 6
10 fun 5758 . . . . . 6
118, 9, 10mp2an 686 . . . . 5
12 axlowdimlem10.1 . . . . . 6
1312feq1i 5730 . . . . 5
1411, 13mpbir 214 . . . 4
15 1re 9660 . . . . . 6
16 snssi 4107 . . . . . 6
1715, 16ax-mp 5 . . . . 5
18 0re 9661 . . . . . 6
19 snssi 4107 . . . . . 6
2018, 19ax-mp 5 . . . . 5
2117, 20unssi 3600 . . . 4
22 fss 5749 . . . 4
2314, 21, 22mp2an 686 . . 3
24 fznatpl1 11876 . . . . . 6
2524snssd 4108 . . . . 5
26 undif 3839 . . . . 5
2725, 26sylib 201 . . . 4
2827feq2d 5725 . . 3
2923, 28mpbii 216 . 2
30 elee 25003 . . 3