isumclimtf - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem isumclimtf 7139

Description: Version of isumclimt 7140 with a bound-variable hypothesis instead of a distinct variable condition.

**Hypotheses**
Ref	Expression
isumclimtf.1	⊢ (y ∈ F → ∀k y ∈ F)
isumclimtf.2	⊢ F ∈ V
isumclimtf.3	⊢ A ∈ V

**Assertion**
Ref	Expression
isumclimtf	⊢ ((M ∈ ℤ ⋀ (⟨M, + ⟩seqF) ⇝ A) → Σk ∈ (ℤ_≥ ‘M)(F ‘k) = A)

Distinct variable groups: y,F y,k

**Proof of Theorem isumclimtf**
Step	Hyp	Ref	Expression
1		isumclimtf.2	. . . 4 ⊢ F ∈ V
2		isumclimtf.1	. . . 4 ⊢ (y ∈ F → ∀k y ∈ F)
3	1, 2	isumvaltf 7137	. . 3 ⊢ (M ∈ ℤ → Σk ∈ (ℤ_≥ ‘M)(F ‘k) = ∪{x∣(⟨M, + ⟩seqF) ⇝ x})
4		rabab 1818	. . . 4 ⊢ {x ∈ V∣(⟨M, + ⟩seqF) ⇝ x} = {x∣(⟨M, + ⟩seqF) ⇝ x}
5	4	unieqi 2506	. . 3 ⊢ ∪{x ∈ V∣(⟨M, + ⟩seqF) ⇝ x} = ∪{x∣(⟨M, + ⟩seqF) ⇝ x}
6	3, 5	syl6eqr 1522	. 2 ⊢ (M ∈ ℤ → Σk ∈ (ℤ_≥ ‘M)(F ‘k) = ∪{x ∈ V∣(⟨M, + ⟩seqF) ⇝ x})
7		isumclimtf.3	. . . . . . 7 ⊢ A ∈ V
8	7	climeu 7045	. . . . . 6 ⊢ ((⟨M, + ⟩seqF) ⇝ A → ∃!x(⟨M, + ⟩seqF) ⇝ x)
9		df-reu 1648	. . . . . . 7 ⊢ (∃!x ∈ V (⟨M, + ⟩seqF) ⇝ x ↔ ∃!x(x ∈ V ⋀ (⟨M, + ⟩seqF) ⇝ x))
10		visset 1809	. . . . . . . . 9 ⊢ x ∈ V
11	10	biantrur 724	. . . . . . . 8 ⊢ ((⟨M, + ⟩seqF) ⇝ x ↔ (x ∈ V ⋀ (⟨M, + ⟩seqF) ⇝ x))
12	11	eubii 1385	. . . . . . 7 ⊢ (∃!x(⟨M, + ⟩seqF) ⇝ x ↔ ∃!x(x ∈ V ⋀ (⟨M, + ⟩seqF) ⇝ x))
13	9, 12	bitr4 176	. . . . . 6 ⊢ (∃!x ∈ V (⟨M, + ⟩seqF) ⇝ x ↔ ∃!x(⟨M, + ⟩seqF) ⇝ x)
14	8, 13	sylibr 200	. . . . 5 ⊢ ((⟨M, + ⟩seqF) ⇝ A → ∃!x ∈ V (⟨M, + ⟩seqF) ⇝ x)
15	14, 7	jctil 292	. . . 4 ⊢ ((⟨M, + ⟩seqF) ⇝ A → (A ∈ V ⋀ ∃!x ∈ V (⟨M, + ⟩seqF) ⇝ x))
16		breq2 2618	. . . . 5 ⊢ (x = A → ((⟨M, + ⟩seqF) ⇝ x ↔ (⟨M, + ⟩seqF) ⇝ A))
17	16	reuuni2 2879	. . . 4 ⊢ ((A ∈ V ⋀ ∃!x ∈ V (⟨M, + ⟩seqF) ⇝ x) → ((⟨M, + ⟩seqF) ⇝ A ↔ ∪{x ∈ V∣(⟨M, + ⟩seqF) ⇝ x} = A))
18	15, 17	syl 10	. . 3 ⊢ ((⟨M, + ⟩seqF) ⇝ A → ((⟨M, + ⟩seqF) ⇝ A ↔ ∪{x ∈ V∣(⟨M, + ⟩seqF) ⇝ x} = A))
19	18	ibi 591	. 2 ⊢ ((⟨M, + ⟩seqF) ⇝ A → ∪{x ∈ V∣(⟨M, + ⟩seqF) ⇝ x} = A)
20	6, 19	sylan9eq 1524	1 ⊢ ((M ∈ ℤ ⋀ (⟨M, + ⟩seqF) ⇝ A) → Σk ∈ (ℤ_≥ ‘M)(F ‘k) = A)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ∀wal 952 = wceq 954 ∈ wcel 956 ∃!weu 1378 {cab 1461 ∃!wreu 1644 {crab 1645 Vcvv 1807 ⟨cop 2407 ∪cuni 2498 class class class wbr 2614 ‘cfv 3177 (class class class)co 3954 + caddc 5217 ℤcz 5278 ℤ_≥cuz 6357 seqcseqz 6471 ⇝ cli 6920 Σcsu 6925

This theorem is referenced by: isumclimt 7140 isumclim2tf 7141 isumclim4t 7144

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-nel 1585 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-en 4357 df-dom 4358 df-sdom 4359 df-sup 4554 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-mp 5069 df-ltp 5070 df-plpr 5144 df-mpr 5145 df-enr 5146 df-nr 5147 df-plr 5148 df-mr 5149 df-ltr 5150 df-0r 5151 df-1r 5152 df-m1r 5153 df-c 5220 df-0 5221 df-1 5222 df-i 5223 df-r 5224 df-plus 5225 df-mul 5226 df-lt 5227 df-sub 5336 df-neg 5338 df-pnf 5467 df-mnf 5468 df-xr 5469 df-ltxr 5470 df-le 5471 df-div 5680 df-n 5881 df-2 5925 df-n0 6055 df-z 6091 df-seq1 6253 df-shft 6286 df-uz 6358 df-fz 6408 df-seqz 6473 df-exp 6509 df-sqr 6608 df-re 6690 df-im 6691 df-cj 6692 df-abs 6693 df-clim 6921 df-sum 6926