carsgclctunlem1 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > carsgclctunlem1		Structured version Visualization version GIF version

Theorem carsgclctunlem1 31793

Description: Lemma for carsgclctun 31797. (Contributed by Thierry Arnoux, 23-May-2020.)

**Hypotheses**
Ref	Expression
carsgval.1	⊢ (𝜑 → 𝑂 ∈ 𝑉)
carsgval.2	⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))
carsgsiga.1	⊢ (𝜑 → (𝑀‘∅) = 0)
carsgsiga.2	⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ^*𝑦 ∈ 𝑥(𝑀‘𝑦))
fiunelcarsg.1	⊢ (𝜑 → 𝐴 ∈ Fin)
fiunelcarsg.2	⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))
carsgclctunlem1.1	⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦)
carsgclctunlem1.2	⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)

**Assertion**
Ref	Expression
carsgclctunlem1	⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ^*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐸,𝑦 𝑥,𝑀,𝑦 𝑥,𝑂,𝑦 𝜑,𝑥,𝑦 Allowed substitution hints: 𝑉(𝑥,𝑦)

Proof of Theorem carsgclctunlem1 Dummy variables 𝑎 𝑒 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4807	. . . . 5 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2	1	ineq2d 4118	. . . 4 ⊢ (𝑎 = ∅ → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ ∅))
3	2	fveq2d 6660	. . 3 ⊢ (𝑎 = ∅ → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ ∅)))
4		esumeq1 31511	. . 3 ⊢ (𝑎 = ∅ → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)))
5	3, 4	eqeq12d 2775	. 2 ⊢ (𝑎 = ∅ → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ ∅)) = Σ^𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦))))
6		unieq 4807	. . . . 5 ⊢ (𝑎 = 𝑏 → ∪ 𝑎 = ∪ 𝑏)
7	6	ineq2d 4118	. . . 4 ⊢ (𝑎 = 𝑏 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝑏))
8	7	fveq2d 6660	. . 3 ⊢ (𝑎 = 𝑏 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
9		esumeq1 31511	. . 3 ⊢ (𝑎 = 𝑏 → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)))
10	8, 9	eqeq12d 2775	. 2 ⊢ (𝑎 = 𝑏 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))))
11		unieq 4807	. . . . 5 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ∪ 𝑎 = ∪ (𝑏 ∪ {𝑥}))
12	11	ineq2d 4118	. . . 4 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ (𝑏 ∪ {𝑥})))
13	12	fveq2d 6660	. . 3 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))))
14		esumeq1 31511	. . 3 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))
15	13, 14	eqeq12d 2775	. 2 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))))
16		unieq 4807	. . . . 5 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴)
17	16	ineq2d 4118	. . . 4 ⊢ (𝑎 = 𝐴 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝐴))
18	17	fveq2d 6660	. . 3 ⊢ (𝑎 = 𝐴 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝐴)))
19		esumeq1 31511	. . 3 ⊢ (𝑎 = 𝐴 → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))
20	18, 19	eqeq12d 2775	. 2 ⊢ (𝑎 = 𝐴 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ^𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦))))
21		carsgsiga.1	. . 3 ⊢ (𝜑 → (𝑀‘∅) = 0)
22		uni0 4826	. . . . . 6 ⊢ ∪ ∅ = ∅
23	22	ineq2i 4115	. . . . 5 ⊢ (𝐸 ∩ ∪ ∅) = (𝐸 ∩ ∅)
24		in0 4286	. . . . 5 ⊢ (𝐸 ∩ ∅) = ∅
25	23, 24	eqtri 2782	. . . 4 ⊢ (𝐸 ∩ ∪ ∅) = ∅
26	25	fveq2i 6659	. . 3 ⊢ (𝑀‘(𝐸 ∩ ∪ ∅)) = (𝑀‘∅)
27		esumnul 31525	. . 3 ⊢ Σ^*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)) = 0
28	21, 26, 27	3eqtr4g 2819	. 2 ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ ∅)) = Σ^*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)))
29		simpr 489	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)))
30	29	eqcomd 2765	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
31		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
32	31	ineq2d 4118	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝐸 ∩ 𝑦) = (𝐸 ∩ 𝑥))
33	32	fveq2d 6660	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
34		simprr 773	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑥 ∈ (𝐴 ∖ 𝑏))
35		carsgval.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))
36	35	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
37		carsgclctunlem1.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)
38	37	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝐸 ∈ 𝒫 𝑂)
39	38	elpwincl1 30386	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ 𝑥) ∈ 𝒫 𝑂)
40	36, 39	ffvelrnd 6841	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘(𝐸 ∩ 𝑥)) ∈ (0[,]+∞))
41	33, 34, 40	esumsn 31542	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
42	41	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
43	30, 42	oveq12d 7166	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
44		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏)))
45		nfcv 2920	. . . . . 6 ⊢ Ⅎ𝑦𝑏
46		nfcv 2920	. . . . . 6 ⊢ Ⅎ𝑦{𝑥}
47		vex 3414	. . . . . . 7 ⊢ 𝑏 ∈ V
48	47	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ∈ V)
49		snex 5298	. . . . . . 7 ⊢ {𝑥} ∈ V
50	49	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → {𝑥} ∈ V)
51	34	eldifbd 3872	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ¬ 𝑥 ∈ 𝑏)
52		disjsn 4602	. . . . . . 7 ⊢ ((𝑏 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝑏)
53	51, 52	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑏 ∩ {𝑥}) = ∅)
54	35	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
55	37	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝐸 ∈ 𝒫 𝑂)
56	55	elpwincl1 30386	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂)
57	54, 56	ffvelrnd 6841	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞))
58	35	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
59	37	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝐸 ∈ 𝒫 𝑂)
60	59	elpwincl1 30386	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂)
61	58, 60	ffvelrnd 6841	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞))
62	44, 45, 46, 48, 50, 53, 57, 61	esumsplit 31530	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))))
63	62	adantr 485	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))))
64		uniun 4821	. . . . . . . 8 ⊢ ∪ (𝑏 ∪ {𝑥}) = (∪ 𝑏 ∪ ∪ {𝑥})
65		vex 3414	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
66	65	unisn 4818	. . . . . . . . 9 ⊢ ∪ {𝑥} = 𝑥
67	66	uneq2i 4066	. . . . . . . 8 ⊢ (∪ 𝑏 ∪ ∪ {𝑥}) = (∪ 𝑏 ∪ 𝑥)
68	64, 67	eqtri 2782	. . . . . . 7 ⊢ ∪ (𝑏 ∪ {𝑥}) = (∪ 𝑏 ∪ 𝑥)
69	68	ineq2i 4115	. . . . . 6 ⊢ (𝐸 ∩ ∪ (𝑏 ∪ {𝑥})) = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))
70	69	fveq2i 6659	. . . . 5 ⊢ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))
71		inass 4125	. . . . . . . . . 10 ⊢ ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏) = (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏))
72		indir 4181	. . . . . . . . . . . 12 ⊢ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏) = ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏))
73		inidm 4124	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑏 ∩ ∪ 𝑏) = ∪ 𝑏
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪ 𝑏 ∩ ∪ 𝑏) = ∪ 𝑏)
75		incom 4107	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑏 ∩ 𝑥) = (𝑥 ∩ ∪ 𝑏)
76		carsgclctunlem1.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦)
77	76	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Disj 𝑦 ∈ 𝐴 𝑦)
78		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ 𝐴)
79	78	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ⊆ 𝐴)
80	77, 79, 34	disjuniel 30448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪ 𝑏 ∩ 𝑥) = ∅)
81	75, 80	syl5eqr 2808	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑥 ∩ ∪ 𝑏) = ∅)
82	74, 81	uneq12d 4070	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏)) = (∪ 𝑏 ∪ ∅))
83		un0 4285	. . . . . . . . . . . . 13 ⊢ (∪ 𝑏 ∪ ∅) = ∪ 𝑏
84	82, 83	eqtrdi 2810	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏)) = ∪ 𝑏)
85	72, 84	syl5eq 2806	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏) = ∪ 𝑏)
86	85	ineq2d 4118	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏)) = (𝐸 ∩ ∪ 𝑏))
87	71, 86	syl5eq 2806	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏) = (𝐸 ∩ ∪ 𝑏))
88	87	fveq2d 6660	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
89		indif2 4176	. . . . . . . . . 10 ⊢ (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏)) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)
90		uncom 4059	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑏 ∪ 𝑥) = (𝑥 ∪ ∪ 𝑏)
91	90	difeq1i 4025	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏)
92		difun2 4375	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏) = (𝑥 ∖ ∪ 𝑏)
93		disj3 4348	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ ↔ 𝑥 = (𝑥 ∖ ∪ 𝑏))
94	93	biimpi 219	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → 𝑥 = (𝑥 ∖ ∪ 𝑏))
95	92, 94	eqtr4id 2813	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏) = 𝑥)
96	91, 95	syl5eq 2806	. . . . . . . . . . . 12 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥)
97	81, 96	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥)
98	97	ineq2d 4118	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏)) = (𝐸 ∩ 𝑥))
99	89, 98	syl5eqr 2808	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏) = (𝐸 ∩ 𝑥))
100	99	fveq2d 6660	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ 𝑥)))
101	88, 100	oveq12d 7166	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
102		carsgval.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ 𝑉)
103	102	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑂 ∈ 𝑉)
104	35	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
105	21	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (𝑀‘∅) = 0)
106		carsgsiga.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ^*𝑦 ∈ 𝑥(𝑀‘𝑦))
107	106	3adant1r 1175	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ^*𝑦 ∈ 𝑥(𝑀‘𝑦))
108		fiunelcarsg.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ Fin)
109		ssfi 8757	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin)
110	108, 109	sylan 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin)
111		fiunelcarsg.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))
112	111	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝐴 ⊆ (toCaraSiga‘𝑀))
113	78, 112	sstrd 3903	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ (toCaraSiga‘𝑀))
114	103, 104, 105, 107, 110, 113	fiunelcarsg 31792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∪ 𝑏 ∈ (toCaraSiga‘𝑀))
115	102, 35	elcarsg 31781	. . . . . . . . . . . 12 ⊢ (𝜑 → (∪ 𝑏 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))))
116	115	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))))
117	114, 116	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)))
118	117	simprd 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))
119	118	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))
120	38	elpwincl1 30386	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∈ 𝒫 𝑂)
121		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))
122	121	ineq1d 4117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∩ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏))
123	122	fveq2d 6660	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∩ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)))
124	121	difeq1d 4028	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∖ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))
125	124	fveq2d 6660	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∖ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)))
126	123, 125	oveq12d 7166	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → ((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))))
127	121	fveq2d 6660	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘𝑒) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
128	126, 127	eqeq12d 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) ↔ ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))))
129	120, 128	rspcdv 3534	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))))
130	119, 129	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
131	101, 130	eqtr3d 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
132	131	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
133	70, 132	eqtr4id 2813	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
134	43, 63, 133	3eqtr4rd 2805	. . 3 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))
135	134	ex 417	. 2 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))))
136	5, 10, 15, 20, 28, 135, 108	findcard2d 8783	1 ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ^*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ∀wral 3071 Vcvv 3410 ∖ cdif 3856 ∪ cun 3857 ∩ cin 3858 ⊆ wss 3859 ∅c0 4226 𝒫 cpw 4492 {csn 4520 ∪ cuni 4796 Disj wdisj 4995 class class class wbr 5030 ⟶wf 6329 ‘cfv 6333 (class class class)co 7148 ωcom 7577 ≼ cdom 8523 Fincfn 8525 0cc0 10565 +∞cpnf 10700 ≤ cle 10704 +_𝑒 cxad 12536 [,]cicc 12772 Σ^*cesum 31504 toCaraSigaccarsg 31777

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7457 ax-inf2 9127 ax-cnex 10621 ax-resscn 10622 ax-1cn 10623 ax-icn 10624 ax-addcl 10625 ax-addrcl 10626 ax-mulcl 10627 ax-mulrcl 10628 ax-mulcom 10629 ax-addass 10630 ax-mulass 10631 ax-distr 10632 ax-i2m1 10633 ax-1ne0 10634 ax-1rid 10635 ax-rnegex 10636 ax-rrecex 10637 ax-cnre 10638 ax-pre-lttri 10639 ax-pre-lttrn 10640 ax-pre-ltadd 10641 ax-pre-mulgt0 10642 ax-pre-sup 10643 ax-addf 10644 ax-mulf 10645

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4419 df-pw 4494 df-sn 4521 df-pr 4523 df-tp 4525 df-op 4527 df-uni 4797 df-int 4837 df-iun 4883 df-iin 4884 df-disj 4996 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5428 df-eprel 5433 df-po 5441 df-so 5442 df-fr 5481 df-se 5482 df-we 5483 df-xp 5528 df-rel 5529 df-cnv 5530 df-co 5531 df-dm 5532 df-rn 5533 df-res 5534 df-ima 5535 df-pred 6124 df-ord 6170 df-on 6171 df-lim 6172 df-suc 6173 df-iota 6292 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-isom 6342 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-of 7403 df-om 7578 df-1st 7691 df-2nd 7692 df-supp 7834 df-wrecs 7955 df-recs 8016 df-rdg 8054 df-1o 8110 df-2o 8111 df-oadd 8114 df-er 8297 df-map 8416 df-pm 8417 df-ixp 8478 df-en 8526 df-dom 8527 df-sdom 8528 df-fin 8529 df-fsupp 8857 df-fi 8898 df-sup 8929 df-inf 8930 df-oi 8997 df-dju 9353 df-card 9391 df-pnf 10705 df-mnf 10706 df-xr 10707 df-ltxr 10708 df-le 10709 df-sub 10900 df-neg 10901 df-div 11326 df-nn 11665 df-2 11727 df-3 11728 df-4 11729 df-5 11730 df-6 11731 df-7 11732 df-8 11733 df-9 11734 df-n0 11925 df-z 12011 df-dec 12128 df-uz 12273 df-q 12379 df-rp 12421 df-xneg 12538 df-xadd 12539 df-xmul 12540 df-ioo 12773 df-ioc 12774 df-ico 12775 df-icc 12776 df-fz 12930 df-fzo 13073 df-fl 13201 df-mod 13277 df-seq 13409 df-exp 13470 df-fac 13674 df-bc 13703 df-hash 13731 df-shft 14464 df-cj 14496 df-re 14497 df-im 14498 df-sqrt 14632 df-abs 14633 df-limsup 14866 df-clim 14883 df-rlim 14884 df-sum 15081 df-ef 15459 df-sin 15461 df-cos 15462 df-pi 15464 df-struct 16533 df-ndx 16534 df-slot 16535 df-base 16537 df-sets 16538 df-ress 16539 df-plusg 16626 df-mulr 16627 df-starv 16628 df-sca 16629 df-vsca 16630 df-ip 16631 df-tset 16632 df-ple 16633 df-ds 16635 df-unif 16636 df-hom 16637 df-cco 16638 df-rest 16744 df-topn 16745 df-0g 16763 df-gsum 16764 df-topgen 16765 df-pt 16766 df-prds 16769 df-ordt 16822 df-xrs 16823 df-qtop 16828 df-imas 16829 df-xps 16831 df-mre 16905 df-mrc 16906 df-acs 16908 df-ps 17866 df-tsr 17867 df-plusf 17907 df-mgm 17908 df-sgrp 17957 df-mnd 17968 df-mhm 18012 df-submnd 18013 df-grp 18162 df-minusg 18163 df-sbg 18164 df-mulg 18282 df-subg 18333 df-cntz 18504 df-cmn 18965 df-abl 18966 df-mgp 19298 df-ur 19310 df-ring 19357 df-cring 19358 df-subrg 19591 df-abv 19646 df-lmod 19694 df-scaf 19695 df-sra 20002 df-rgmod 20003 df-psmet 20148 df-xmet 20149 df-met 20150 df-bl 20151 df-mopn 20152 df-fbas 20153 df-fg 20154 df-cnfld 20157 df-top 21584 df-topon 21601 df-topsp 21623 df-bases 21636 df-cld 21709 df-ntr 21710 df-cls 21711 df-nei 21788 df-lp 21826 df-perf 21827 df-cn 21917 df-cnp 21918 df-haus 22005 df-tx 22252 df-hmeo 22445 df-fil 22536 df-fm 22628 df-flim 22629 df-flf 22630 df-tmd 22762 df-tgp 22763 df-tsms 22817 df-trg 22850 df-xms 23012 df-ms 23013 df-tms 23014 df-nm 23274 df-ngp 23275 df-nrg 23277 df-nlm 23278 df-ii 23568 df-cncf 23569 df-limc 24555 df-dv 24556 df-log 25237 df-esum 31505 df-carsg 31778

This theorem is referenced by: carsggect 31794 carsgclctunlem2 31795

W3C validator