bj-finsumval0

Description: Value of a finite sum. (Contributed by BJ, 9-Jun-2019) (Proof shortened by AV, 5-May-2021)

	Ref	Expression
Hypotheses	bj-finsumval0.1	⊢ ( 𝜑 → 𝐴 ∈ CMnd )
	bj-finsumval0.2	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	bj-finsumval0.3	⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) )
Assertion	bj-finsumval0	⊢ ( 𝜑 → ( 𝐴 FinSum 𝐵 ) = ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-finsumval0.1	⊢ ( 𝜑 → 𝐴 ∈ CMnd )
2		bj-finsumval0.2	⊢ ( 𝜑 → 𝐼 ∈ Fin )
3		bj-finsumval0.3	⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) )
4		df-ov	⊢ ( 𝐴 FinSum 𝐵 ) = ( FinSum ‘ ⟨ 𝐴 , 𝐵 ⟩ )
5		df-bj-finsum	⊢ FinSum = ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↦ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ )
7	6	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → 𝐴 ∈ CMnd )
9	3 2	fexd	⊢ ( 𝜑 → 𝐵 ∈ V )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → 𝐵 ∈ V )
11		op1stg	⊢ ( ( 𝐴 ∈ CMnd ∧ 𝐵 ∈ V ) → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
12	8 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
13	7 12	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 1^st ‘ 𝑥 ) = 𝐴 )
14	6	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
15		op2ndg	⊢ ( ( 𝐴 ∈ CMnd ∧ 𝐵 ∈ V ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
16	8 10 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
17	14 16	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 2^nd ‘ 𝑥 ) = 𝐵 )
18	17	dmeqd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → dom ( 2^nd ‘ 𝑥 ) = dom 𝐵 )
19	3	fdmd	⊢ ( 𝜑 → dom 𝐵 = 𝐼 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → dom 𝐵 = 𝐼 )
21	18 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → dom ( 2^nd ‘ 𝑥 ) = 𝐼 )
22		f1oeq3	⊢ ( dom ( 2^nd ‘ 𝑥 ) = 𝐼 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ↔ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ) )
23	22	biimpd	⊢ ( dom ( 2^nd ‘ 𝑥 ) = 𝐼 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ) )
24	23	ad2antll	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ) )
25	24	adantrd	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ) )
26	25	adantr	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ) )
27		eqidd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 1 = 1 )
28		simprl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) → ( 1^st ‘ 𝑥 ) = 𝐴 )
29	28	fveq2d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) → ( +_g ‘ ( 1^st ‘ 𝑥 ) ) = ( +_g ‘ 𝐴 ) )
30	29	adantrr	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( +_g ‘ ( 1^st ‘ 𝑥 ) ) = ( +_g ‘ 𝐴 ) )
31		simprrl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) → ( 2^nd ‘ 𝑥 ) = 𝐵 )
32	31	adantr	⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ 𝑥 ) = 𝐵 )
33	32	fveq1d	⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) )
34	33	mpteq2dva	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
35	34	adantrr	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
36	27 30 35	seqeq123d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
37		simprr	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → dom ( 2^nd ‘ 𝑥 ) = 𝐼 )
38	37	anim1ci	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) )
39		hashfz1	⊢ ( 𝑚 ∈ ℕ₀ → ( ♯ ‘ ( 1 ... 𝑚 ) ) = 𝑚 )
40	39	eqcomd	⊢ ( 𝑚 ∈ ℕ₀ → 𝑚 = ( ♯ ‘ ( 1 ... 𝑚 ) ) )
41	40	ad2antrl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → 𝑚 = ( ♯ ‘ ( 1 ... 𝑚 ) ) )
42		fzfid	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( 1 ... 𝑚 ) ∈ Fin )
43		19.8a	⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) → ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) )
44	43	adantr	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) )
45		hasheqf1oi	⊢ ( ( 1 ... 𝑚 ) ∈ Fin → ( ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) → ( ♯ ‘ ( 1 ... 𝑚 ) ) = ( ♯ ‘ dom ( 2^nd ‘ 𝑥 ) ) ) )
46	42 44 45	sylc	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( ♯ ‘ ( 1 ... 𝑚 ) ) = ( ♯ ‘ dom ( 2^nd ‘ 𝑥 ) ) )
47		simprr	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → dom ( 2^nd ‘ 𝑥 ) = 𝐼 )
48	47	fveq2d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( ♯ ‘ dom ( 2^nd ‘ 𝑥 ) ) = ( ♯ ‘ 𝐼 ) )
49	41 46 48	3eqtrd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( 𝑚 ∈ ℕ₀ ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → 𝑚 = ( ♯ ‘ 𝐼 ) )
50	38 49	sylan2	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 𝑚 = ( ♯ ‘ 𝐼 ) )
51	36 50	fveq12d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) )
52	51	eqeq2d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ↔ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) )
53	52	biimpd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) → 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) )
54	53	impancom	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) → ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) )
55	54	com12	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) → 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) )
56	26 55	jcad	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
57	22	biimprd	⊢ ( dom ( 2^nd ‘ 𝑥 ) = 𝐼 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ) )
58	57	ad2antll	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ) )
59	58	adantr	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ) )
60	59	adantrd	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ) )
61		eqidd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 1 = 1 )
62		simpl	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( 1^st ‘ 𝑥 ) = 𝐴 )
63		tru	⊢ ⊤
64	62 63	jctir	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ⊤ ) )
65	64	ad2antrl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ⊤ ) )
66		simpl	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ⊤ ) → ( 1^st ‘ 𝑥 ) = 𝐴 )
67	66	eqcomd	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ⊤ ) → 𝐴 = ( 1^st ‘ 𝑥 ) )
68	65 67	syl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 𝐴 = ( 1^st ‘ 𝑥 ) )
69	68	fveq2d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( +_g ‘ 𝐴 ) = ( +_g ‘ ( 1^st ‘ 𝑥 ) ) )
70		simpl	⊢ ( ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) → ( 2^nd ‘ 𝑥 ) = 𝐵 )
71	70	eqcomd	⊢ ( ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) → 𝐵 = ( 2^nd ‘ 𝑥 ) )
72	71	ad2antll	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) → 𝐵 = ( 2^nd ‘ 𝑥 ) )
73	72	adantr	⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐵 = ( 2^nd ‘ 𝑥 ) )
74	73	fveq1d	⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
75	74	adantlrr	⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
76	75	mpteq2dva	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
77	61 69 76	seqeq123d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
78	59	impcom	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) )
79		simprr	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 𝑚 ∈ ℕ₀ )
80	37	ad2antrl	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → dom ( 2^nd ‘ 𝑥 ) = 𝐼 )
81	78 79 80 49	syl12anc	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → 𝑚 = ( ♯ ‘ 𝐼 ) )
82	81	eqcomd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( ♯ ‘ 𝐼 ) = 𝑚 )
83	77 82	fveq12d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) )
84	83	eqeq2d	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ↔ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) )
85	84	biimpd	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) ) → ( 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) → 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) )
86	85	impancom	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) → ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) )
87	86	com12	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) → 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) )
88	60 87	jcad	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) )
89	56 88	impbid	⊢ ( ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
90	89	ex	⊢ ( ( ( 1^st ‘ 𝑥 ) = 𝐴 ∧ ( ( 2^nd ‘ 𝑥 ) = 𝐵 ∧ dom ( 2^nd ‘ 𝑥 ) = 𝐼 ) ) → ( 𝑚 ∈ ℕ₀ → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
91	13 17 21 90	syl12anc	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝑚 ∈ ℕ₀ → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
92	91	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) ∧ 𝑚 ∈ ℕ₀ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
93	92	exbidv	⊢ ( ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) ∧ 𝑚 ∈ ℕ₀ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
94	93	rexbidva	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
95	94	iotabidv	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ dom ( 2^nd ‘ 𝑥 ) ∧ 𝑠 = ( seq 1 ( ( +_g ‘ ( 1^st ‘ 𝑥 ) ) , ( 𝑛 ∈ ℕ ↦ ( ( 2^nd ‘ 𝑥 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) ) ) = ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
96		eleq1	⊢ ( 𝑡 = 𝐼 → ( 𝑡 ∈ Fin ↔ 𝐼 ∈ Fin ) )
97		feq2	⊢ ( 𝑡 = 𝐼 → ( 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ↔ 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) ) )
98	96 97	anbi12d	⊢ ( 𝑡 = 𝐼 → ( ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ↔ ( 𝐼 ∈ Fin ∧ 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) ) ) )
99	98	ceqsexgv	⊢ ( 𝐼 ∈ Fin → ( ∃ 𝑡 ( 𝑡 = 𝐼 ∧ ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) ↔ ( 𝐼 ∈ Fin ∧ 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) ) ) )
100	2 99	syl	⊢ ( 𝜑 → ( ∃ 𝑡 ( 𝑡 = 𝐼 ∧ ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) ↔ ( 𝐼 ∈ Fin ∧ 𝐵 : 𝐼 ⟶ ( Base ‘ 𝐴 ) ) ) )
101	2 3 100	mpbir2and	⊢ ( 𝜑 → ∃ 𝑡 ( 𝑡 = 𝐼 ∧ ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) )
102		exsimpr	⊢ ( ∃ 𝑡 ( 𝑡 = 𝐼 ∧ ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) → ∃ 𝑡 ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
103	101 102	syl	⊢ ( 𝜑 → ∃ 𝑡 ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
104		df-rex	⊢ ( ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ↔ ∃ 𝑡 ( 𝑡 ∈ Fin ∧ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
105	103 104	sylibr	⊢ ( 𝜑 → ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) )
106		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ CMnd ↔ 𝐴 ∈ CMnd ) )
107		fveq2	⊢ ( 𝑦 = 𝐴 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝐴 ) )
108	107	feq3d	⊢ ( 𝑦 = 𝐴 → ( 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ↔ 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
109	108	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ↔ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
110	106 109	anbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) ↔ ( 𝐴 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) )
111		feq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ↔ 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
112	111	rexbidv	⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ↔ ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) )
113	112	anbi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ↔ ( 𝐴 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) )
114	110 113	opelopabg	⊢ ( ( 𝐴 ∈ CMnd ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↔ ( 𝐴 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) )
115	1 9 114	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } ↔ ( 𝐴 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝐵 : 𝑡 ⟶ ( Base ‘ 𝐴 ) ) ) )
116	1 105 115	mpbir2and	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ CMnd ∧ ∃ 𝑡 ∈ Fin 𝑧 : 𝑡 ⟶ ( Base ‘ 𝑦 ) ) } )
117		iotaex	⊢ ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ V
118	117	a1i	⊢ ( 𝜑 → ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ V )
119	5 95 116 118	fvmptd2	⊢ ( 𝜑 → ( FinSum ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
120	4 119	syl5eq	⊢ ( 𝜑 → ( 𝐴 FinSum 𝐵 ) = ( ℩ 𝑠 ∃ 𝑚 ∈ ℕ₀ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐼 ∧ 𝑠 = ( seq 1 ( ( +_g ‘ 𝐴 ) , ( 𝑛 ∈ ℕ ↦ ( 𝐵 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ‘ ( ♯ ‘ 𝐼 ) ) ) ) )

Metamath Proof Explorer

Theorem bj-finsumval0

Proof