Metamath Proof Explorer

Theorem upgrwlkdvdelem

Description: Lemma for upgrwlkdvde . (Contributed by Alexander van der Vekens, 27-Oct-2017) (Proof shortened by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvdelem ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ 𝐹 ∈ Word dom 𝐼 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → Fun ◡ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 wrdfin ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 ∈ Fin )
2 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
3 simpr ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
4 3 adantr ⊢ ( ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
5 2fveq3 ⊢ ( 𝑘 = 𝑥 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
6 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑥 ) )
7 fvoveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) )
8 6 7 preq12d ⊢ ( 𝑘 = 𝑥 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
9 5 8 eqeq12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
10 9 rspcv ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
11 2fveq3 ⊢ ( 𝑘 = 𝑦 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) )
12 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑦 ) )
13 fvoveq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) )
14 12 13 preq12d ⊢ ( 𝑘 = 𝑦 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } )
15 11 14 eqeq12d ⊢ ( 𝑘 = 𝑦 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) )
16 15 rspcv ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) )
17 10 16 anim12ii ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) )
18 fveq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) )
19 simpl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
20 19 eqcomd ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
21 20 adantl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
22 simpl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) )
23 simpr ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } )
24 23 adantl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } )
25 21 22 24 3eqtrd ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } )
26 fvex ⊢ ( 𝑃 ‘ 𝑥 ) ∈ V
27 fvex ⊢ ( 𝑃 ‘ ( 𝑥 + 1 ) ) ∈ V
28 fvex ⊢ ( 𝑃 ‘ 𝑦 ) ∈ V
29 fvex ⊢ ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∈ V
30 26 27 28 29 preq12b ⊢ ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ↔ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) ∨ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) )
31 dff13 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ↔ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
32 elfzofz ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
33 elfzofz ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑦 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
34 fveqeq2 ⊢ ( 𝑎 = 𝑥 → ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) ↔ ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) ) )
35 eqeq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 = 𝑏 ↔ 𝑥 = 𝑏 ) )
36 34 35 imbi12d ⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) → 𝑥 = 𝑏 ) ) )
37 fveq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑃 ‘ 𝑏 ) = ( 𝑃 ‘ 𝑦 ) )
38 37 eqeq2d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) ↔ ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ) )
39 eqeq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑥 = 𝑏 ↔ 𝑥 = 𝑦 ) )
40 38 39 imbi12d ⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) → 𝑥 = 𝑏 ) ↔ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
41 36 40 rspc2v ⊢ ( ( 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
42 32 33 41 syl2an ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
43 42 a1dd ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
44 43 com14 ⊢ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
45 44 adantr ⊢ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
46 hashcl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
47 32 a1i ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
48 fzofzp1 ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑦 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
49 47 48 anim12d1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( 𝑦 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ) )
50 49 imp ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( 𝑦 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
51 fveq2 ⊢ ( 𝑏 = ( 𝑦 + 1 ) → ( 𝑃 ‘ 𝑏 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) )
52 51 eqeq2d ⊢ ( 𝑏 = ( 𝑦 + 1 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) ↔ ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) )
53 eqeq2 ⊢ ( 𝑏 = ( 𝑦 + 1 ) → ( 𝑥 = 𝑏 ↔ 𝑥 = ( 𝑦 + 1 ) ) )
54 52 53 imbi12d ⊢ ( 𝑏 = ( 𝑦 + 1 ) → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑏 ) → 𝑥 = 𝑏 ) ↔ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) → 𝑥 = ( 𝑦 + 1 ) ) ) )
55 36 54 rspc2v ⊢ ( ( 𝑥 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( 𝑦 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) → 𝑥 = ( 𝑦 + 1 ) ) ) )
56 50 55 syl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) → 𝑥 = ( 𝑦 + 1 ) ) ) )
57 56 imp ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) → 𝑥 = ( 𝑦 + 1 ) ) )
58 fzofzp1 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑥 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
59 58 a1i ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑥 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
60 59 33 anim12d1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑥 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ) )
61 60 imp ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑥 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
62 fveqeq2 ⊢ ( 𝑎 = ( 𝑥 + 1 ) → ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) ↔ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑏 ) ) )
63 eqeq1 ⊢ ( 𝑎 = ( 𝑥 + 1 ) → ( 𝑎 = 𝑏 ↔ ( 𝑥 + 1 ) = 𝑏 ) )
64 62 63 imbi12d ⊢ ( 𝑎 = ( 𝑥 + 1 ) → ( ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑏 ) → ( 𝑥 + 1 ) = 𝑏 ) ) )
65 37 eqeq2d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑏 ) ↔ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) )
66 eqeq2 ⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 + 1 ) = 𝑏 ↔ ( 𝑥 + 1 ) = 𝑦 ) )
67 65 66 imbi12d ⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑏 ) → ( 𝑥 + 1 ) = 𝑏 ) ↔ ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) → ( 𝑥 + 1 ) = 𝑦 ) ) )
68 64 67 rspc2v ⊢ ( ( ( 𝑥 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) → ( 𝑥 + 1 ) = 𝑦 ) ) )
69 61 68 syl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) → ( 𝑥 + 1 ) = 𝑦 ) ) )
70 69 imp ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) → ( ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) → ( 𝑥 + 1 ) = 𝑦 ) )
71 57 70 anim12d ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) → ( 𝑥 = ( 𝑦 + 1 ) ∧ ( 𝑥 + 1 ) = 𝑦 ) ) )
72 71 expimpd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( 𝑥 = ( 𝑦 + 1 ) ∧ ( 𝑥 + 1 ) = 𝑦 ) ) )
73 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 + 1 ) = ( ( 𝑦 + 1 ) + 1 ) )
74 73 eqeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( ( 𝑦 + 1 ) + 1 ) = 𝑦 ) )
75 74 adantl ⊢ ( ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( ( 𝑦 + 1 ) + 1 ) = 𝑦 ) )
76 elfzonn0 ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑦 ∈ ℕ0 )
77 nn0cn ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℂ )
78 add1p1 ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 + 1 ) + 1 ) = ( 𝑦 + 2 ) )
79 77 78 syl ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝑦 + 1 ) + 1 ) = ( 𝑦 + 2 ) )
80 79 eqeq1d ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 + 1 ) + 1 ) = 𝑦 ↔ ( 𝑦 + 2 ) = 𝑦 ) )
81 2cnd ⊢ ( 𝑦 ∈ ℕ0 → 2 ∈ ℂ )
82 2ne0 ⊢ 2 ≠ 0
83 82 a1i ⊢ ( 𝑦 ∈ ℕ0 → 2 ≠ 0 )
84 addn0nid ⊢ ( ( 𝑦 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑦 + 2 ) ≠ 𝑦 )
85 77 81 83 84 syl3anc ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 2 ) ≠ 𝑦 )
86 eqneqall ⊢ ( ( 𝑦 + 2 ) = 𝑦 → ( ( 𝑦 + 2 ) ≠ 𝑦 → 𝑥 = 𝑦 ) )
87 85 86 syl5com ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝑦 + 2 ) = 𝑦 → 𝑥 = 𝑦 ) )
88 80 87 sylbid ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 + 1 ) + 1 ) = 𝑦 → 𝑥 = 𝑦 ) )
89 76 88 syl ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝑦 + 1 ) + 1 ) = 𝑦 → 𝑥 = 𝑦 ) )
90 89 adantl ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑦 + 1 ) + 1 ) = 𝑦 → 𝑥 = 𝑦 ) )
91 90 adantr ⊢ ( ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( ( 𝑦 + 1 ) + 1 ) = 𝑦 → 𝑥 = 𝑦 ) )
92 75 91 sylbid ⊢ ( ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑥 = ( 𝑦 + 1 ) ) → ( ( 𝑥 + 1 ) = 𝑦 → 𝑥 = 𝑦 ) )
93 92 expimpd ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑥 = ( 𝑦 + 1 ) ∧ ( 𝑥 + 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) )
94 93 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑥 = ( 𝑦 + 1 ) ∧ ( 𝑥 + 1 ) = 𝑦 ) → 𝑥 = 𝑦 ) )
95 72 94 syld ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
96 95 ex ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ) )
97 46 96 syl ⊢ ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ) )
98 97 com3l ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ∧ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( 𝐹 ∈ Fin → 𝑥 = 𝑦 ) ) )
99 98 expd ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) → ( 𝐹 ∈ Fin → 𝑥 = 𝑦 ) ) ) )
100 99 com34 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) ) ) )
101 100 com14 ⊢ ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
102 45 101 jaoi ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) ∨ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
103 102 adantld ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) ∨ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∀ 𝑏 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( ( 𝑃 ‘ 𝑎 ) = ( 𝑃 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
104 31 103 biimtrid ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) ∨ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
105 104 com23 ⊢ ( ( ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑦 ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ) ∨ ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑦 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 𝑦 ) ) ) → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
106 30 105 sylbi ⊢ ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
107 25 106 syl ⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) ) → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) )
108 107 ex ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) ) )
109 18 108 syl ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑥 = 𝑦 ) ) ) ) )
110 109 com15 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) = { ( 𝑃 ‘ 𝑦 ) , ( 𝑃 ‘ ( 𝑦 + 1 ) ) } ) → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
111 17 110 syld ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( 𝐹 ∈ Fin → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
112 111 com14 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
113 112 imp ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝐹 ∈ Fin → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
114 113 impcom ⊢ ( ( 𝐹 ∈ Fin ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
115 114 ralrimivv ⊢ ( ( 𝐹 ∈ Fin ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
116 115 adantlr ⊢ ( ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
117 dff13 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
118 4 116 117 sylanbrc ⊢ ( ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
119 df-f1 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun ◡ 𝐹 ) )
120 118 119 sylib ⊢ ( ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun ◡ 𝐹 ) )
121 simpr ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ∧ Fun ◡ 𝐹 ) → Fun ◡ 𝐹 )
122 120 121 syl ⊢ ( ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) ∧ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) → Fun ◡ 𝐹 )
123 122 ex ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → Fun ◡ 𝐹 ) )
124 123 expd ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → Fun ◡ 𝐹 ) ) )
125 1 2 124 syl2anc ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → Fun ◡ 𝐹 ) ) )
126 125 impcom ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) –1-1→ 𝑉 ∧ 𝐹 ∈ Word dom 𝐼 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → Fun ◡ 𝐹 ) )