Metamath Proof Explorer


Theorem gsumval3eu

Description: The group sum as defined in gsumval3a is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014)

Ref Expression
Hypotheses gsumval3.b 𝐵 = ( Base ‘ 𝐺 )
gsumval3.0 0 = ( 0g𝐺 )
gsumval3.p + = ( +g𝐺 )
gsumval3.z 𝑍 = ( Cntz ‘ 𝐺 )
gsumval3.g ( 𝜑𝐺 ∈ Mnd )
gsumval3.a ( 𝜑𝐴𝑉 )
gsumval3.f ( 𝜑𝐹 : 𝐴𝐵 )
gsumval3.c ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumval3a.t ( 𝜑𝑊 ∈ Fin )
gsumval3a.n ( 𝜑𝑊 ≠ ∅ )
gsumval3a.s ( 𝜑𝑊𝐴 )
Assertion gsumval3eu ( 𝜑 → ∃! 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumval3.0 0 = ( 0g𝐺 )
3 gsumval3.p + = ( +g𝐺 )
4 gsumval3.z 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumval3.g ( 𝜑𝐺 ∈ Mnd )
6 gsumval3.a ( 𝜑𝐴𝑉 )
7 gsumval3.f ( 𝜑𝐹 : 𝐴𝐵 )
8 gsumval3.c ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumval3a.t ( 𝜑𝑊 ∈ Fin )
10 gsumval3a.n ( 𝜑𝑊 ≠ ∅ )
11 gsumval3a.s ( 𝜑𝑊𝐴 )
12 10 neneqd ( 𝜑 → ¬ 𝑊 = ∅ )
13 fz1f1o ( 𝑊 ∈ Fin → ( 𝑊 = ∅ ∨ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) )
14 9 13 syl ( 𝜑 → ( 𝑊 = ∅ ∨ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) )
15 14 ord ( 𝜑 → ( ¬ 𝑊 = ∅ → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) )
16 12 15 mpd ( 𝜑 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) )
17 16 simprd ( 𝜑 → ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
18 excom ( ∃ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑓𝑥 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
19 exancom ( ∃ 𝑥 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑥 ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) )
20 fvex ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∈ V
21 biidd ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) )
22 20 21 ceqsexv ( ∃ 𝑥 ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
23 19 22 bitri ( ∃ 𝑥 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
24 23 exbii ( ∃ 𝑓𝑥 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
25 18 24 bitri ( ∃ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
26 17 25 sylibr ( 𝜑 → ∃ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
27 exdistrv ( ∃ 𝑓𝑔 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
28 an4 ( ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ∧ ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
29 5 adantr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝐺 ∈ Mnd )
30 1 3 mndcl ( ( 𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
31 30 3expb ( ( 𝐺 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
32 29 31 sylan ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
33 8 adantr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
34 33 sselda ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑥 ∈ ran 𝐹 ) → 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) )
35 34 adantrr ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ ( 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 ) ) → 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) )
36 simprr ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ ( 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 ) ) → 𝑦 ∈ ran 𝐹 )
37 3 4 cntzi ( ( 𝑥 ∈ ( 𝑍 ‘ ran 𝐹 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
38 35 36 37 syl2anc ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ ( 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
39 1 3 mndass ( ( 𝐺 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
40 29 39 sylan ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
41 16 simpld ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
42 41 adantr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
43 nnuz ℕ = ( ℤ ‘ 1 )
44 42 43 eleqtrdi ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ ‘ 1 ) )
45 7 adantr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝐹 : 𝐴𝐵 )
46 45 frnd ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ran 𝐹𝐵 )
47 simprr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
48 f1ocnv ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 𝑔 : 𝑊1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
49 47 48 syl ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑔 : 𝑊1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
50 simprl ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 )
51 f1oco ( ( 𝑔 : 𝑊1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) → ( 𝑔𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
52 49 50 51 syl2anc ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( 𝑔𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
53 f1of ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
54 47 53 syl ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
55 fvco3 ( ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑔 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑔𝑥 ) ) )
56 54 55 sylan ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑔 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑔𝑥 ) ) )
57 45 ffnd ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝐹 Fn 𝐴 )
58 11 adantr ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑊𝐴 )
59 54 58 fssd ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
60 59 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑔𝑥 ) ∈ 𝐴 )
61 fnfvelrn ( ( 𝐹 Fn 𝐴 ∧ ( 𝑔𝑥 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑔𝑥 ) ) ∈ ran 𝐹 )
62 57 60 61 syl2an2r ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑔𝑥 ) ) ∈ ran 𝐹 )
63 56 62 eqeltrd ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑔 ) ‘ 𝑥 ) ∈ ran 𝐹 )
64 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
65 50 64 syl ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊 )
66 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑔𝑓 ) ‘ 𝑘 ) = ( 𝑔 ‘ ( 𝑓𝑘 ) ) )
67 65 66 sylan ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑔𝑓 ) ‘ 𝑘 ) = ( 𝑔 ‘ ( 𝑓𝑘 ) ) )
68 67 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑔 ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) = ( 𝑔 ‘ ( 𝑔 ‘ ( 𝑓𝑘 ) ) ) )
69 65 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓𝑘 ) ∈ 𝑊 )
70 f1ocnvfv2 ( ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ∧ ( 𝑓𝑘 ) ∈ 𝑊 ) → ( 𝑔 ‘ ( 𝑔 ‘ ( 𝑓𝑘 ) ) ) = ( 𝑓𝑘 ) )
71 47 69 70 syl2an2r ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑔 ‘ ( 𝑔 ‘ ( 𝑓𝑘 ) ) ) = ( 𝑓𝑘 ) )
72 68 71 eqtr2d ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓𝑘 ) = ( 𝑔 ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) )
73 72 fveq2d ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑓𝑘 ) ) = ( 𝐹 ‘ ( 𝑔 ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) ) )
74 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝑊𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑓𝑘 ) ) )
75 65 74 sylan ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑓𝑘 ) ) )
76 f1of ( ( 𝑔𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑔𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
77 52 76 syl ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( 𝑔𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
78 77 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑔𝑓 ) ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
79 fvco3 ( ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ∧ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑔 ) ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑔 ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) ) )
80 59 78 79 syl2an2r ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑔 ) ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝑔 ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) ) )
81 73 75 80 3eqtr4d ( ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑘 ) = ( ( 𝐹𝑔 ) ‘ ( ( 𝑔𝑓 ) ‘ 𝑘 ) ) )
82 32 38 40 44 46 52 63 81 seqf1o ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
83 eqeq12 ( ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑥 = 𝑦 ↔ ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
84 82 83 syl5ibrcom ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ) → ( ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 = 𝑦 ) )
85 84 expimpd ( 𝜑 → ( ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) ∧ ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∧ 𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) )
86 28 85 syl5bir ( 𝜑 → ( ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) )
87 86 exlimdvv ( 𝜑 → ( ∃ 𝑓𝑔 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) )
88 27 87 syl5bir ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) )
89 88 alrimivv ( 𝜑 → ∀ 𝑥𝑦 ( ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) )
90 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ↔ 𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
91 90 anbi2d ( 𝑥 = 𝑦 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
92 91 exbidv ( 𝑥 = 𝑦 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
93 f1oeq1 ( 𝑓 = 𝑔 → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊 ) )
94 coeq2 ( 𝑓 = 𝑔 → ( 𝐹𝑓 ) = ( 𝐹𝑔 ) )
95 94 seqeq3d ( 𝑓 = 𝑔 → seq 1 ( + , ( 𝐹𝑓 ) ) = seq 1 ( + , ( 𝐹𝑔 ) ) )
96 95 fveq1d ( 𝑓 = 𝑔 → ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
97 96 eqeq2d ( 𝑓 = 𝑔 → ( 𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ↔ 𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
98 93 97 anbi12d ( 𝑓 = 𝑔 → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
99 98 cbvexvw ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
100 92 99 bitrdi ( 𝑥 = 𝑦 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
101 100 eu4 ( ∃! 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ↔ ( ∃ 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ∀ 𝑥𝑦 ( ( ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑦 = ( seq 1 ( + , ( 𝐹𝑔 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑥 = 𝑦 ) ) )
102 26 89 101 sylanbrc ( 𝜑 → ∃! 𝑥𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto𝑊𝑥 = ( seq 1 ( + , ( 𝐹𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )