| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gsumval3.h | . . . . . . 7
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) | 
| 2 |  | f1f 6804 | . . . . . . 7
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)⟶𝐴) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐻:(1...𝑀)⟶𝐴) | 
| 4 |  | fzfid 14014 | . . . . . 6
⊢ (𝜑 → (1...𝑀) ∈ Fin) | 
| 5 | 3, 4 | fexd 7247 | . . . . 5
⊢ (𝜑 → 𝐻 ∈ V) | 
| 6 |  | vex 3484 | . . . . 5
⊢ 𝑓 ∈ V | 
| 7 |  | coexg 7951 | . . . . 5
⊢ ((𝐻 ∈ V ∧ 𝑓 ∈ V) → (𝐻 ∘ 𝑓) ∈ V) | 
| 8 | 5, 6, 7 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝐻 ∘ 𝑓) ∈ V) | 
| 9 | 8 | ad2antrr 726 | . . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓) ∈ V) | 
| 10 |  | gsumval3.b | . . . . 5
⊢ 𝐵 = (Base‘𝐺) | 
| 11 |  | gsumval3.0 | . . . . 5
⊢  0 =
(0g‘𝐺) | 
| 12 |  | gsumval3.p | . . . . 5
⊢  + =
(+g‘𝐺) | 
| 13 |  | gsumval3.z | . . . . 5
⊢ 𝑍 = (Cntz‘𝐺) | 
| 14 |  | gsumval3.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ Mnd) | 
| 15 |  | gsumval3.a | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 16 |  | gsumval3.f | . . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 17 |  | gsumval3.c | . . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | 
| 18 |  | gsumval3.m | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 19 |  | gsumval3.n | . . . . 5
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) | 
| 20 |  | gsumval3.w | . . . . 5
⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) | 
| 21 | 10, 11, 12, 13, 14, 15, 16, 17, 18, 1, 19, 20 | gsumval3lem1 19923 | . . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) | 
| 22 |  | fzfi 14013 | . . . . . . . 8
⊢
(1...𝑀) ∈
Fin | 
| 23 |  | suppssdm 8202 | . . . . . . . . . 10
⊢ ((𝐹 ∘ 𝐻) supp 0 ) ⊆ dom (𝐹 ∘ 𝐻) | 
| 24 | 20, 23 | eqsstri 4030 | . . . . . . . . 9
⊢ 𝑊 ⊆ dom (𝐹 ∘ 𝐻) | 
| 25 | 16, 3 | fcod 6761 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 ∘ 𝐻):(1...𝑀)⟶𝐵) | 
| 26 | 24, 25 | fssdm 6755 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ⊆ (1...𝑀)) | 
| 27 |  | ssfi 9213 | . . . . . . . 8
⊢
(((1...𝑀) ∈ Fin
∧ 𝑊 ⊆ (1...𝑀)) → 𝑊 ∈ Fin) | 
| 28 | 22, 26, 27 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) | 
| 29 | 28 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ∈ Fin) | 
| 30 | 1 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐻:(1...𝑀)–1-1→𝐴) | 
| 31 | 26 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝑊 ⊆ (1...𝑀)) | 
| 32 |  | f1ores 6862 | . . . . . . . 8
⊢ ((𝐻:(1...𝑀)–1-1→𝐴 ∧ 𝑊 ⊆ (1...𝑀)) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊)) | 
| 34 | 20 | imaeq2i 6076 | . . . . . . . . . 10
⊢ (𝐻 “ 𝑊) = (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) | 
| 35 | 16, 15 | fexd 7247 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) | 
| 36 |  | ovex 7464 | . . . . . . . . . . . . . 14
⊢
(1...𝑀) ∈
V | 
| 37 |  | fex 7246 | . . . . . . . . . . . . . 14
⊢ ((𝐻:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐻 ∈ V) | 
| 38 | 3, 36, 37 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ V) | 
| 39 | 35, 38 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐻 ∈ V)) | 
| 40 |  | f1fun 6806 | . . . . . . . . . . . . . 14
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → Fun 𝐻) | 
| 41 | 1, 40 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐻) | 
| 42 | 41, 19 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻)) | 
| 43 |  | imacosupp 8234 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((Fun 𝐻 ∧ (𝐹 supp 0 ) ⊆ ran 𝐻) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 ))) | 
| 44 | 39, 42, 43 | sylc 65 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) | 
| 45 | 44 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ ((𝐹 ∘ 𝐻) supp 0 )) = (𝐹 supp 0 )) | 
| 46 | 34, 45 | eqtrid 2789 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) | 
| 47 | 46 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 “ 𝑊) = (𝐹 supp 0 )) | 
| 48 | 47 | f1oeq3d 6845 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐻 “ 𝑊) ↔ (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 ))) | 
| 49 | 33, 48 | mpbid 232 | . . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐻 ↾ 𝑊):𝑊–1-1-onto→(𝐹 supp 0 )) | 
| 50 | 29, 49 | hasheqf1od 14392 | . . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) →
(♯‘𝑊) =
(♯‘(𝐹 supp
0
))) | 
| 51 | 50 | fveq2d 6910 | . . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) | 
| 52 | 21, 51 | jca 511 | . . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))) | 
| 53 |  | f1oeq1 6836 | . . . 4
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ↔ (𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) | 
| 54 |  | coeq2 5869 | . . . . . . 7
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝐻 ∘ 𝑓))) | 
| 55 | 54 | seqeq3d 14050 | . . . . . 6
⊢ (𝑔 = (𝐻 ∘ 𝑓) → seq1( + , (𝐹 ∘ 𝑔)) = seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))) | 
| 56 | 55 | fveq1d 6908 | . . . . 5
⊢ (𝑔 = (𝐻 ∘ 𝑓) → (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) | 
| 57 | 56 | eqeq2d 2748 | . . . 4
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 ))))) | 
| 58 | 53, 57 | anbi12d 632 | . . 3
⊢ (𝑔 = (𝐻 ∘ 𝑓) → ((𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ ((𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))))) | 
| 59 | 9, 52, 58 | spcedv 3598 | . 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) | 
| 60 | 14 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐺 ∈ Mnd) | 
| 61 | 15 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐴 ∈ 𝑉) | 
| 62 | 16 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → 𝐹:𝐴⟶𝐵) | 
| 63 | 17 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | 
| 64 |  | f1f1orn 6859 | . . . . . . . . . . . . 13
⊢ (𝐻:(1...𝑀)–1-1→𝐴 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) | 
| 65 | 1, 64 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) | 
| 66 |  | f1oen3g 9007 | . . . . . . . . . . . 12
⊢ ((𝐻 ∈ V ∧ 𝐻:(1...𝑀)–1-1-onto→ran
𝐻) → (1...𝑀) ≈ ran 𝐻) | 
| 67 | 5, 65, 66 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (1...𝑀) ≈ ran 𝐻) | 
| 68 |  | enfi 9227 | . . . . . . . . . . 11
⊢
((1...𝑀) ≈ ran
𝐻 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((1...𝑀) ∈ Fin ↔ ran 𝐻 ∈ Fin)) | 
| 70 | 22, 69 | mpbii 233 | . . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ∈ Fin) | 
| 71 | 70, 19 | ssfid 9301 | . . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) | 
| 72 | 71 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ∈
Fin) | 
| 73 | 20 | neeq1i 3005 | . . . . . . . . . 10
⊢ (𝑊 ≠ ∅ ↔ ((𝐹 ∘ 𝐻) supp 0 ) ≠
∅) | 
| 74 |  | supp0cosupp0 8233 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → ((𝐹 supp 0 ) = ∅ → ((𝐹 ∘ 𝐻) supp 0 ) =
∅)) | 
| 75 | 74 | necon3d 2961 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) | 
| 76 | 35, 38, 75 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐹 ∘ 𝐻) supp 0 ) ≠ ∅ →
(𝐹 supp 0 ) ≠
∅)) | 
| 77 | 73, 76 | biimtrid 242 | . . . . . . . . 9
⊢ (𝜑 → (𝑊 ≠ ∅ → (𝐹 supp 0 ) ≠
∅)) | 
| 78 | 77 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 ≠ ∅) → (𝐹 supp 0 ) ≠
∅) | 
| 79 | 78 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ≠
∅) | 
| 80 | 19 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ⊆ ran 𝐻) | 
| 81 | 3 | frnd 6744 | . . . . . . . . 9
⊢ (𝜑 → ran 𝐻 ⊆ 𝐴) | 
| 82 | 81 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ran 𝐻 ⊆ 𝐴) | 
| 83 | 80, 82 | sstrd 3994 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐹 supp 0 ) ⊆ 𝐴) | 
| 84 | 10, 11, 12, 13, 60, 61, 62, 63, 72, 79, 83 | gsumval3eu 19922 | . . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∃!𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) | 
| 85 |  | iota1 6538 | . . . . . 6
⊢
(∃!𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) = 𝑥)) | 
| 86 | 84, 85 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) = 𝑥)) | 
| 87 |  | eqid 2737 | . . . . . . 7
⊢ (𝐹 supp 0 ) = (𝐹 supp 0 ) | 
| 88 |  | simprl 771 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ¬ 𝐴 ∈ ran
...) | 
| 89 | 10, 11, 12, 13, 60, 61, 62, 63, 72, 79, 87, 88 | gsumval3a 19921 | . . . . . 6
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))))) | 
| 90 | 89 | eqeq1d 2739 | . . . . 5
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ((𝐺 Σg
𝐹) = 𝑥 ↔ (℩𝑥∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) = 𝑥)) | 
| 91 | 86, 90 | bitr4d 282 | . . . 4
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) | 
| 92 | 91 | alrimiv 1927 | . . 3
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → ∀𝑥(∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥)) | 
| 93 |  | fvex 6919 | . . . 4
⊢ (seq1(
+ ,
(𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) ∈ V | 
| 94 |  | eqeq1 2741 | . . . . . . 7
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → (𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))) ↔ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 ))))) | 
| 95 | 94 | anbi2d 630 | . . . . . 6
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → ((𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))))) | 
| 96 | 95 | exbidv 1921 | . . . . 5
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ ∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))))) | 
| 97 |  | eqeq2 2749 | . . . . 5
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → ((𝐺 Σg 𝐹) = 𝑥 ↔ (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) | 
| 98 | 96, 97 | bibi12d 345 | . . . 4
⊢ (𝑥 = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) → ((∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥) ↔ (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))))) | 
| 99 | 93, 98 | spcv 3605 | . . 3
⊢
(∀𝑥(∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = 𝑥) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) | 
| 100 | 92, 99 | syl 17 | . 2
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (∃𝑔(𝑔:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) ∧ (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)) = (seq1( + , (𝐹 ∘ 𝑔))‘(♯‘(𝐹 supp 0 )))) ↔ (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊)))) | 
| 101 | 59, 100 | mpbid 232 | 1
⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , <
((1...(♯‘𝑊)),
𝑊))) → (𝐺 Σg
𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(♯‘𝑊))) |