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 ⊢ 𝐹 = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ if ( 𝑖 = 1 , ( { ⟨ 3 , - 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { 3 } ) × { 0 } ) ) , ( { ⟨ ( 𝑖 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝑖 + 1 ) } ) × { 0 } ) ) ) )
Assertion axlowdimlem15 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) –1-1→ ( 𝔼 ‘ 𝑁 ) )

Proof

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