Step | Hyp | Ref
| Expression |
1 | | df-ov 6552 |
. 2
⊢ (𝐴 FinSum 𝐵) = ( FinSum ‘〈𝐴, 𝐵〉) |
2 | | df-bj-finsum 32323 |
. . . 4
⊢ FinSum =
(𝑥 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → FinSum = (𝑥 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))) |
4 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝑥 = 〈𝐴, 𝐵〉) |
5 | 4 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st ‘𝑥) = (1st
‘〈𝐴, 𝐵〉)) |
6 | | bj-finsumval0.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ CMnd) |
7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝐴 ∈ CMnd) |
8 | | bj-finsumval0.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵:𝐼⟶(Base‘𝐴)) |
9 | | bj-finsumval0.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ Fin) |
10 | | fex 6394 |
. . . . . . . . . . . 12
⊢ ((𝐵:𝐼⟶(Base‘𝐴) ∧ 𝐼 ∈ Fin) → 𝐵 ∈ V) |
11 | 8, 9, 10 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ V) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝐵 ∈ V) |
13 | | op1stg 7071 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) →
(1st ‘〈𝐴, 𝐵〉) = 𝐴) |
14 | 7, 12, 13 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st
‘〈𝐴, 𝐵〉) = 𝐴) |
15 | 5, 14 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st ‘𝑥) = 𝐴) |
16 | 4 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd ‘𝑥) = (2nd
‘〈𝐴, 𝐵〉)) |
17 | | op2ndg 7072 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) →
(2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
18 | 7, 12, 17 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd
‘〈𝐴, 𝐵〉) = 𝐵) |
19 | 16, 18 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd ‘𝑥) = 𝐵) |
20 | 19 | dmeqd 5248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom (2nd
‘𝑥) = dom 𝐵) |
21 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐵:𝐼⟶(Base‘𝐴) → dom 𝐵 = 𝐼) |
22 | 8, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐵 = 𝐼) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom 𝐵 = 𝐼) |
24 | 20, 23 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom (2nd
‘𝑥) = 𝐼) |
25 | | f1oeq3 6042 |
. . . . . . . . . . . . . . 15
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
↔ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
26 | 25 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
27 | 26 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
28 | 27 | adantrd 483 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
29 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
30 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 1 =
1) |
31 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (1st ‘𝑥) = 𝐴) |
32 | 31 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) →
(+g‘(1st ‘𝑥)) = (+g‘𝐴)) |
33 | 32 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(+g‘(1st ‘𝑥)) = (+g‘𝐴)) |
34 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (2nd ‘𝑥) = 𝐵) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → (2nd
‘𝑥) = 𝐵) |
36 | 35 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → ((2nd
‘𝑥)‘(𝑓‘𝑛)) = (𝐵‘(𝑓‘𝑛))) |
37 | 36 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) |
38 | 37 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) |
39 | 30, 33, 38 | seqeq123d 12672 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) = seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
41 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → dom (2nd ‘𝑥) = 𝐼) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → dom
(2nd ‘𝑥) =
𝐼) |
43 | 40, 42 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → (𝑚 ∈ ℕ0
∧ dom (2nd ‘𝑥) = 𝐼)) |
44 | | hashfz1 12996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ0
→ (#‘(1...𝑚)) =
𝑚) |
45 | 44 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ0
→ 𝑚 =
(#‘(1...𝑚))) |
46 | 45 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → 𝑚 = (#‘(1...𝑚))) |
47 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (1...𝑚) ∈ Fin) |
48 | | 19.8a 2039 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → ∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
50 | | hasheqf1oi 13002 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1...𝑚) ∈ Fin
→ (∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ (#‘(1...𝑚)) =
(#‘dom (2nd ‘𝑥)))) |
51 | 47, 49, 50 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (#‘(1...𝑚)) = (#‘dom (2nd
‘𝑥))) |
52 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → dom (2nd ‘𝑥) = 𝐼) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (#‘dom (2nd
‘𝑥)) = (#‘𝐼)) |
54 | 46, 51, 53 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → 𝑚 = (#‘𝐼)) |
55 | 43, 54 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 = (#‘𝐼)) |
56 | 39, 55 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))) |
57 | 56 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) ↔ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) |
58 | 57 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) → 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) |
59 | 58 | impancom 455 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → ((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) |
60 | 59 | com12 32 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) |
61 | 29, 60 | jcad 554 |
. . . . . . . . . 10
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
62 | 25 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
63 | 62 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
64 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
65 | 64 | adantrd 483 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))) → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
66 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 1 =
1) |
67 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (1st ‘𝑥) = 𝐴) |
68 | | tru 1479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⊤ |
69 | 67, 68 | jctir 559 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → ((1st ‘𝑥) = 𝐴 ∧ ⊤)) |
70 | 69 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
((1st ‘𝑥)
= 𝐴 ∧
⊤)) |
71 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑥) = 𝐴 ∧ ⊤) → (1st
‘𝑥) = 𝐴) |
72 | 71 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) = 𝐴 ∧ ⊤) → 𝐴 = (1st ‘𝑥)) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝐴 = (1st ‘𝑥)) |
74 | 73 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(+g‘𝐴) =
(+g‘(1st ‘𝑥))) |
75 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼) → (2nd ‘𝑥) = 𝐵) |
76 | 75 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼) → 𝐵 = (2nd ‘𝑥)) |
77 | 76 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) → 𝐵 = (2nd ‘𝑥)) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → 𝐵 = (2nd ‘𝑥)) |
79 | 78 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → (𝐵‘(𝑓‘𝑛)) = ((2nd ‘𝑥)‘(𝑓‘𝑛))) |
80 | 79 | adantlrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) ∧ 𝑛 ∈ ℕ) → (𝐵‘(𝑓‘𝑛)) = ((2nd ‘𝑥)‘(𝑓‘𝑛))) |
81 | 80 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) |
82 | 66, 74, 81 | seqeq123d 12672 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) =
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))) |
83 | 64 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
84 | | simprr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 ∈
ℕ0) |
85 | 41 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → dom
(2nd ‘𝑥) =
𝐼) |
86 | 83, 84, 85, 54 | syl12anc 1316 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 = (#‘𝐼)) |
87 | 86 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(#‘𝐼) = 𝑚) |
88 | 82, 87 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)) =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
89 | 88 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)) ↔ 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
90 | 89 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)) → 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
91 | 90 | impancom 455 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))) → ((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
92 | 91 | com12 32 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))) → 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
93 | 65, 92 | jcad 554 |
. . . . . . . . . 10
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))) → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |
94 | 61, 93 | impbid 201 |
. . . . . . . . 9
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
95 | 94 | ex 449 |
. . . . . . . 8
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑚 ∈ ℕ0 → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))))) |
96 | 15, 19, 24, 95 | syl12anc 1316 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (𝑚 ∈ ℕ0 → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))))) |
97 | 96 | imp 444 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
98 | 97 | exbidv 1837 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) ∧ 𝑚 ∈ ℕ0) →
(∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
99 | 98 | rexbidva 3031 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
100 | 99 | iotabidv 5789 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
101 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐼 → (𝑡 ∈ Fin ↔ 𝐼 ∈ Fin)) |
102 | | feq2 5940 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐼 → (𝐵:𝑡⟶(Base‘𝐴) ↔ 𝐵:𝐼⟶(Base‘𝐴))) |
103 | 101, 102 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑡 = 𝐼 → ((𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴)) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
104 | 103 | ceqsexgv 3305 |
. . . . . . . 8
⊢ (𝐼 ∈ Fin → (∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
105 | 9, 104 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
106 | 9, 8, 105 | mpbir2and 959 |
. . . . . 6
⊢ (𝜑 → ∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴)))) |
107 | | exsimpr 1784 |
. . . . . 6
⊢
(∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) → ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
108 | 106, 107 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
109 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑡 ∈ Fin
𝐵:𝑡⟶(Base‘𝐴) ↔ ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
110 | 108, 109 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)) |
111 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 ∈ CMnd ↔ 𝐴 ∈ CMnd)) |
112 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (Base‘𝑦) = (Base‘𝐴)) |
113 | 112 | feq3d 5945 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑧:𝑡⟶(Base‘𝑦) ↔ 𝑧:𝑡⟶(Base‘𝐴))) |
114 | 113 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦) ↔ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴))) |
115 | 111, 114 | anbi12d 743 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)) ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴)))) |
116 | | feq1 5939 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑧:𝑡⟶(Base‘𝐴) ↔ 𝐵:𝑡⟶(Base‘𝐴))) |
117 | 116 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴) ↔ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴))) |
118 | 117 | anbi2d 736 |
. . . . . 6
⊢ (𝑧 = 𝐵 → ((𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴)) ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
119 | 115, 118 | opelopabg 4918 |
. . . . 5
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
120 | 6, 11, 119 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
121 | 6, 110, 120 | mpbir2and 959 |
. . 3
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}) |
122 | | iotaex 5785 |
. . . 4
⊢
(℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) ∈ V |
123 | 122 | a1i 11 |
. . 3
⊢ (𝜑 → (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))) ∈ V) |
124 | 3, 100, 121, 123 | fvmptd 6197 |
. 2
⊢ (𝜑 → ( FinSum
‘〈𝐴, 𝐵〉) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |
125 | 1, 124 | syl5eq 2656 |
1
⊢ (𝜑 → (𝐴 FinSum 𝐵) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) |