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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( 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 biimtrrid ⊢ ( 𝜑 → ( ( ( 𝑓 : ( 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 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑓 ( 𝑓 : ( 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 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )