Step | Hyp | Ref
| Expression |
1 | | df-ov 7024 |
. 2
⊢ (𝐴 FinSum 𝐵) = ( FinSum ‘〈𝐴, 𝐵〉) |
2 | | df-bj-finsum 34144 |
. . . 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 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝑥 = 〈𝐴, 𝐵〉) |
5 | 4 | fveq2d 6547 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st ‘𝑥) = (1st
‘〈𝐴, 𝐵〉)) |
6 | | bj-finsumval0.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ CMnd) |
7 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝐴 ∈ CMnd) |
8 | | bj-finsumval0.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵:𝐼⟶(Base‘𝐴)) |
9 | | bj-finsumval0.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ Fin) |
10 | | fex 6860 |
. . . . . . . . . . . 12
⊢ ((𝐵:𝐼⟶(Base‘𝐴) ∧ 𝐼 ∈ Fin) → 𝐵 ∈ V) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ V) |
12 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → 𝐵 ∈ V) |
13 | | op1stg 7562 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) →
(1st ‘〈𝐴, 𝐵〉) = 𝐴) |
14 | 7, 12, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st
‘〈𝐴, 𝐵〉) = 𝐴) |
15 | 5, 14 | eqtrd 2831 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (1st ‘𝑥) = 𝐴) |
16 | 4 | fveq2d 6547 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd ‘𝑥) = (2nd
‘〈𝐴, 𝐵〉)) |
17 | | op2ndg 7563 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) →
(2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
18 | 7, 12, 17 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd
‘〈𝐴, 𝐵〉) = 𝐵) |
19 | 16, 18 | eqtrd 2831 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (2nd ‘𝑥) = 𝐵) |
20 | 19 | dmeqd 5665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom (2nd
‘𝑥) = dom 𝐵) |
21 | 8 | fdmd 6396 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐵 = 𝐼) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom 𝐵 = 𝐼) |
23 | 20, 22 | eqtrd 2831 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → dom (2nd
‘𝑥) = 𝐼) |
24 | | f1oeq3 6479 |
. . . . . . . . . . . . . . 15
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
↔ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
25 | 24 | biimpd 230 |
. . . . . . . . . . . . . 14
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
26 | 25 | ad2antll 725 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
27 | 26 | adantrd 492 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑓:(1...𝑚)–1-1-onto→𝐼)) |
29 | | eqidd 2796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 1 =
1) |
30 | | simprl 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (1st ‘𝑥) = 𝐴) |
31 | 30 | fveq2d 6547 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) →
(+g‘(1st ‘𝑥)) = (+g‘𝐴)) |
32 | 31 | adantrr 713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(+g‘(1st ‘𝑥)) = (+g‘𝐴)) |
33 | | simprrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (2nd ‘𝑥) = 𝐵) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → (2nd
‘𝑥) = 𝐵) |
35 | 34 | fveq1d 6545 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → ((2nd
‘𝑥)‘(𝑓‘𝑛)) = (𝐵‘(𝑓‘𝑛))) |
36 | 35 | mpteq2dva 5060 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ ((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼))) → (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) |
37 | 36 | adantrr 713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) |
38 | 29, 32, 37 | seqeq123d 13233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) = seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))) |
39 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
40 | | simprr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → dom (2nd ‘𝑥) = 𝐼) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → dom
(2nd ‘𝑥) =
𝐼) |
42 | 39, 41 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → (𝑚 ∈ ℕ0
∧ dom (2nd ‘𝑥) = 𝐼)) |
43 | | hashfz1 13561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ0
→ (♯‘(1...𝑚)) = 𝑚) |
44 | 43 | eqcomd 2801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ0
→ 𝑚 =
(♯‘(1...𝑚))) |
45 | 44 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → 𝑚 = (♯‘(1...𝑚))) |
46 | | fzfid 13196 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (1...𝑚) ∈ Fin) |
47 | | 19.8a 2144 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → ∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
49 | | hasheqf1oi 13567 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1...𝑚) ∈ Fin
→ (∃𝑓 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
→ (♯‘(1...𝑚)) = (♯‘dom (2nd
‘𝑥)))) |
50 | 46, 48, 49 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (♯‘(1...𝑚)) = (♯‘dom
(2nd ‘𝑥))) |
51 | | simprr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → dom (2nd ‘𝑥) = 𝐼) |
52 | 51 | fveq2d 6547 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → (♯‘dom (2nd
‘𝑥)) =
(♯‘𝐼)) |
53 | 45, 50, 52 | 3eqtrd 2835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (𝑚 ∈
ℕ0 ∧ dom (2nd ‘𝑥) = 𝐼)) → 𝑚 = (♯‘𝐼)) |
54 | 42, 53 | sylan2 592 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 = (♯‘𝐼)) |
55 | 38, 54 | fveq12d 6550 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))) |
56 | 55 | eqeq2d 2805 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) ↔ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) |
57 | 56 | biimpd 230 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ (((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚) → 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) |
58 | 57 | impancom 452 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → ((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) |
59 | 58 | com12 32 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) |
60 | 28, 59 | jcad 513 |
. . . . . . . . . 10
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) → (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
61 | 24 | biimprd 249 |
. . . . . . . . . . . . . 14
⊢ (dom
(2nd ‘𝑥) =
𝐼 → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
62 | 61 | ad2antll 725 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
63 | 62 | adantr 481 |
. . . . . . . . . . . 12
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → (𝑓:(1...𝑚)–1-1-onto→𝐼 → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
64 | 63 | adantrd 492 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))) → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥))) |
65 | | eqidd 2796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 1 =
1) |
66 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (1st ‘𝑥) = 𝐴) |
67 | | tru 1526 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⊤ |
68 | 66, 67 | jctir 521 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → ((1st ‘𝑥) = 𝐴 ∧ ⊤)) |
69 | 68 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
((1st ‘𝑥)
= 𝐴 ∧
⊤)) |
70 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑥) = 𝐴 ∧ ⊤) → (1st
‘𝑥) = 𝐴) |
71 | 70 | eqcomd 2801 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑥) = 𝐴 ∧ ⊤) → 𝐴 = (1st ‘𝑥)) |
72 | 69, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝐴 = (1st ‘𝑥)) |
73 | 72 | fveq2d 6547 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(+g‘𝐴) =
(+g‘(1st ‘𝑥))) |
74 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼) → (2nd ‘𝑥) = 𝐵) |
75 | 74 | eqcomd 2801 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼) → 𝐵 = (2nd ‘𝑥)) |
76 | 75 | ad2antll 725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) → 𝐵 = (2nd ‘𝑥)) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → 𝐵 = (2nd ‘𝑥)) |
78 | 77 | fveq1d 6545 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ ((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼))) ∧ 𝑛 ∈ ℕ) → (𝐵‘(𝑓‘𝑛)) = ((2nd ‘𝑥)‘(𝑓‘𝑛))) |
79 | 78 | adantlrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) ∧ 𝑛 ∈ ℕ) → (𝐵‘(𝑓‘𝑛)) = ((2nd ‘𝑥)‘(𝑓‘𝑛))) |
80 | 79 | mpteq2dva 5060 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛)))) |
81 | 65, 73, 80 | seqeq123d 13233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛)))) =
seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))) |
82 | 63 | impcom 408 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)) |
83 | | simprr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 ∈
ℕ0) |
84 | 40 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → dom
(2nd ‘𝑥) =
𝐼) |
85 | 82, 83, 84, 53 | syl12anc 833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → 𝑚 = (♯‘𝐼)) |
86 | 85 | eqcomd 2801 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(♯‘𝐼) = 𝑚) |
87 | 81, 86 | fveq12d 6550 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) →
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)) =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) |
88 | 87 | eqeq2d 2805 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)) ↔ 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
89 | 88 | biimpd 230 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ (((1st
‘𝑥) = 𝐴 ∧ ((2nd
‘𝑥) = 𝐵 ∧ dom (2nd
‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0)) → (𝑠 =
(seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)) → 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
90 | 89 | impancom 452 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))) → ((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
91 | 90 | com12 32 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))) → 𝑠 = (seq1((+g‘(1st
‘𝑥)), (𝑛 ∈ ℕ ↦
((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) |
92 | 64, 91 | jcad 513 |
. . . . . . . . . 10
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))) → (𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) |
93 | 60, 92 | impbid 213 |
. . . . . . . . 9
⊢
((((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
94 | 93 | ex 413 |
. . . . . . . 8
⊢
(((1st ‘𝑥) = 𝐴 ∧ ((2nd ‘𝑥) = 𝐵 ∧ dom (2nd ‘𝑥) = 𝐼)) → (𝑚 ∈ ℕ0 → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))))) |
95 | 15, 19, 23, 94 | syl12anc 833 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (𝑚 ∈ ℕ0 → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))))) |
96 | 95 | imp 407 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) ∧ 𝑚 ∈ ℕ0) → ((𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
97 | 96 | exbidv 1899 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) ∧ 𝑚 ∈ ℕ0) →
(∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
98 | 97 | rexbidva 3259 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚)) ↔ ∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
99 | 98 | iotabidv 6215 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 〈𝐴, 𝐵〉) → (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom
(2nd ‘𝑥)
∧ 𝑠 =
(seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd
‘𝑥)‘(𝑓‘𝑛))))‘𝑚))) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
100 | | eleq1 2870 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐼 → (𝑡 ∈ Fin ↔ 𝐼 ∈ Fin)) |
101 | | feq2 6369 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐼 → (𝐵:𝑡⟶(Base‘𝐴) ↔ 𝐵:𝐼⟶(Base‘𝐴))) |
102 | 100, 101 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑡 = 𝐼 → ((𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴)) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
103 | 102 | ceqsexgv 3586 |
. . . . . . . 8
⊢ (𝐼 ∈ Fin → (∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
104 | 9, 103 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) ↔ (𝐼 ∈ Fin ∧ 𝐵:𝐼⟶(Base‘𝐴)))) |
105 | 9, 8, 104 | mpbir2and 709 |
. . . . . 6
⊢ (𝜑 → ∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴)))) |
106 | | exsimpr 1851 |
. . . . . 6
⊢
(∃𝑡(𝑡 = 𝐼 ∧ (𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) → ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
108 | | df-rex 3111 |
. . . . 5
⊢
(∃𝑡 ∈ Fin
𝐵:𝑡⟶(Base‘𝐴) ↔ ∃𝑡(𝑡 ∈ Fin ∧ 𝐵:𝑡⟶(Base‘𝐴))) |
109 | 107, 108 | sylibr 235 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)) |
110 | | eleq1 2870 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 ∈ CMnd ↔ 𝐴 ∈ CMnd)) |
111 | | fveq2 6543 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (Base‘𝑦) = (Base‘𝐴)) |
112 | 111 | feq3d 6374 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑧:𝑡⟶(Base‘𝑦) ↔ 𝑧:𝑡⟶(Base‘𝐴))) |
113 | 112 | rexbidv 3260 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦) ↔ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴))) |
114 | 110, 113 | anbi12d 630 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦)) ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴)))) |
115 | | feq1 6368 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑧:𝑡⟶(Base‘𝐴) ↔ 𝐵:𝑡⟶(Base‘𝐴))) |
116 | 115 | rexbidv 3260 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴) ↔ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴))) |
117 | 116 | anbi2d 628 |
. . . . . 6
⊢ (𝑧 = 𝐵 → ((𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝐴)) ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
118 | 114, 117 | opelopabg 5320 |
. . . . 5
⊢ ((𝐴 ∈ CMnd ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
119 | 6, 11, 118 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↔ (𝐴 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝐵:𝑡⟶(Base‘𝐴)))) |
120 | 6, 109, 119 | mpbir2and 709 |
. . 3
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))}) |
121 | | iotaex 6211 |
. . . 4
⊢
(℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) ∈ V |
122 | 121 | a1i 11 |
. . 3
⊢ (𝜑 → (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))) ∈ V) |
123 | 3, 99, 120, 122 | fvmptd 6646 |
. 2
⊢ (𝜑 → ( FinSum
‘〈𝐴, 𝐵〉) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |
124 | 1, 123 | syl5eq 2843 |
1
⊢ (𝜑 → (𝐴 FinSum 𝐵) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼))))) |