Metamath Proof Explorer


Theorem axlowdimlem15

Description: Lemma for axlowdim . Set up a one-to-one function of points. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypothesis axlowdimlem15.1 F = i 1 N 1 if i = 1 3 1 1 N 3 × 0 i + 1 1 1 N i + 1 × 0
Assertion axlowdimlem15 N 3 F : 1 N 1 1-1 𝔼 N

Proof

Step Hyp Ref Expression
1 axlowdimlem15.1 F = i 1 N 1 if i = 1 3 1 1 N 3 × 0 i + 1 1 1 N i + 1 × 0
2 eqid 3 1 1 N 3 × 0 = 3 1 1 N 3 × 0
3 2 axlowdimlem7 N 3 3 1 1 N 3 × 0 𝔼 N
4 3 adantr N 3 i 1 N 1 3 1 1 N 3 × 0 𝔼 N
5 eluzge3nn N 3 N
6 eqid i + 1 1 1 N i + 1 × 0 = i + 1 1 1 N i + 1 × 0
7 6 axlowdimlem10 N i 1 N 1 i + 1 1 1 N i + 1 × 0 𝔼 N
8 5 7 sylan N 3 i 1 N 1 i + 1 1 1 N i + 1 × 0 𝔼 N
9 4 8 ifcld N 3 i 1 N 1 if i = 1 3 1 1 N 3 × 0 i + 1 1 1 N i + 1 × 0 𝔼 N
10 9 1 fmptd N 3 F : 1 N 1 𝔼 N
11 eqeq1 i = j i = 1 j = 1
12 oveq1 i = j i + 1 = j + 1
13 12 opeq1d i = j i + 1 1 = j + 1 1
14 13 sneqd i = j i + 1 1 = j + 1 1
15 12 sneqd i = j i + 1 = j + 1
16 15 difeq2d i = j 1 N i + 1 = 1 N j + 1
17 16 xpeq1d i = j 1 N i + 1 × 0 = 1 N j + 1 × 0
18 14 17 uneq12d i = j i + 1 1 1 N i + 1 × 0 = j + 1 1 1 N j + 1 × 0
19 11 18 ifbieq2d i = j if i = 1 3 1 1 N 3 × 0 i + 1 1 1 N i + 1 × 0 = if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0
20 snex 3 1 V
21 ovex 1 N V
22 21 difexi 1 N 3 V
23 snex 0 V
24 22 23 xpex 1 N 3 × 0 V
25 20 24 unex 3 1 1 N 3 × 0 V
26 snex j + 1 1 V
27 21 difexi 1 N j + 1 V
28 27 23 xpex 1 N j + 1 × 0 V
29 26 28 unex j + 1 1 1 N j + 1 × 0 V
30 25 29 ifex if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 V
31 19 1 30 fvmpt j 1 N 1 F j = if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0
32 eqeq1 i = k i = 1 k = 1
33 oveq1 i = k i + 1 = k + 1
34 33 opeq1d i = k i + 1 1 = k + 1 1
35 34 sneqd i = k i + 1 1 = k + 1 1
36 33 sneqd i = k i + 1 = k + 1
37 36 difeq2d i = k 1 N i + 1 = 1 N k + 1
38 37 xpeq1d i = k 1 N i + 1 × 0 = 1 N k + 1 × 0
39 35 38 uneq12d i = k i + 1 1 1 N i + 1 × 0 = k + 1 1 1 N k + 1 × 0
40 32 39 ifbieq2d i = k if i = 1 3 1 1 N 3 × 0 i + 1 1 1 N i + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0
41 snex k + 1 1 V
42 21 difexi 1 N k + 1 V
43 42 23 xpex 1 N k + 1 × 0 V
44 41 43 unex k + 1 1 1 N k + 1 × 0 V
45 25 44 ifex if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 V
46 40 1 45 fvmpt k 1 N 1 F k = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0
47 31 46 eqeqan12d j 1 N 1 k 1 N 1 F j = F k if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0
48 47 adantl N 3 j 1 N 1 k 1 N 1 F j = F k if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0
49 eqtr3 j = 1 k = 1 j = k
50 49 2a1d j = 1 k = 1 N 3 j 1 N 1 k 1 N 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k
51 eqid k + 1 1 1 N k + 1 × 0 = k + 1 1 1 N k + 1 × 0
52 2 51 axlowdimlem13 N k 1 N 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0
53 52 neneqd N k 1 N 1 ¬ 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0
54 53 pm2.21d N k 1 N 1 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0 j = k
55 54 adantrl N j 1 N 1 k 1 N 1 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0 j = k
56 5 55 sylan N 3 j 1 N 1 k 1 N 1 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0 j = k
57 iftrue j = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0
58 iffalse ¬ k = 1 if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 = k + 1 1 1 N k + 1 × 0
59 57 58 eqeqan12d j = 1 ¬ k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0
60 59 imbi1d j = 1 ¬ k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k 3 1 1 N 3 × 0 = k + 1 1 1 N k + 1 × 0 j = k
61 56 60 syl5ibr j = 1 ¬ k = 1 N 3 j 1 N 1 k 1 N 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k
62 eqid j + 1 1 1 N j + 1 × 0 = j + 1 1 1 N j + 1 × 0
63 2 62 axlowdimlem13 N j 1 N 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0
64 63 necomd N j 1 N 1 j + 1 1 1 N j + 1 × 0 3 1 1 N 3 × 0
65 64 neneqd N j 1 N 1 ¬ j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0
66 65 pm2.21d N j 1 N 1 j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0 j = k
67 5 66 sylan N 3 j 1 N 1 j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0 j = k
68 67 adantrr N 3 j 1 N 1 k 1 N 1 j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0 j = k
69 iffalse ¬ j = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = j + 1 1 1 N j + 1 × 0
70 iftrue k = 1 if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 = 3 1 1 N 3 × 0
71 69 70 eqeqan12d ¬ j = 1 k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0
72 71 imbi1d ¬ j = 1 k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k j + 1 1 1 N j + 1 × 0 = 3 1 1 N 3 × 0 j = k
73 68 72 syl5ibr ¬ j = 1 k = 1 N 3 j 1 N 1 k 1 N 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k
74 62 51 axlowdimlem14 N j 1 N 1 k 1 N 1 j + 1 1 1 N j + 1 × 0 = k + 1 1 1 N k + 1 × 0 j = k
75 74 3expb N j 1 N 1 k 1 N 1 j + 1 1 1 N j + 1 × 0 = k + 1 1 1 N k + 1 × 0 j = k
76 5 75 sylan N 3 j 1 N 1 k 1 N 1 j + 1 1 1 N j + 1 × 0 = k + 1 1 1 N k + 1 × 0 j = k
77 69 58 eqeqan12d ¬ j = 1 ¬ k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j + 1 1 1 N j + 1 × 0 = k + 1 1 1 N k + 1 × 0
78 77 imbi1d ¬ j = 1 ¬ k = 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k j + 1 1 1 N j + 1 × 0 = k + 1 1 1 N k + 1 × 0 j = k
79 76 78 syl5ibr ¬ j = 1 ¬ k = 1 N 3 j 1 N 1 k 1 N 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k
80 50 61 73 79 4cases N 3 j 1 N 1 k 1 N 1 if j = 1 3 1 1 N 3 × 0 j + 1 1 1 N j + 1 × 0 = if k = 1 3 1 1 N 3 × 0 k + 1 1 1 N k + 1 × 0 j = k
81 48 80 sylbid N 3 j 1 N 1 k 1 N 1 F j = F k j = k
82 81 ralrimivva N 3 j 1 N 1 k 1 N 1 F j = F k j = k
83 dff13 F : 1 N 1 1-1 𝔼 N F : 1 N 1 𝔼 N j 1 N 1 k 1 N 1 F j = F k j = k
84 10 82 83 sylanbrc N 3 F : 1 N 1 1-1 𝔼 N