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 32284

Description: Lemma for carsgclctun 32288. (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 4850	. . . . 5 ⊢ (𝑎 = ∅ → ∪ 𝑎 = ∪ ∅)
2	1	ineq2d 4146	. . . 4 ⊢ (𝑎 = ∅ → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ ∅))
3	2	fveq2d 6778	. . 3 ⊢ (𝑎 = ∅ → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ ∅)))
4		esumeq1 32002	. . 3 ⊢ (𝑎 = ∅ → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)))
5	3, 4	eqeq12d 2754	. 2 ⊢ (𝑎 = ∅ → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ ∅)) = Σ^𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦))))
6		unieq 4850	. . . . 5 ⊢ (𝑎 = 𝑏 → ∪ 𝑎 = ∪ 𝑏)
7	6	ineq2d 4146	. . . 4 ⊢ (𝑎 = 𝑏 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝑏))
8	7	fveq2d 6778	. . 3 ⊢ (𝑎 = 𝑏 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
9		esumeq1 32002	. . 3 ⊢ (𝑎 = 𝑏 → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)))
10	8, 9	eqeq12d 2754	. 2 ⊢ (𝑎 = 𝑏 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))))
11		unieq 4850	. . . . 5 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ∪ 𝑎 = ∪ (𝑏 ∪ {𝑥}))
12	11	ineq2d 4146	. . . 4 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ (𝑏 ∪ {𝑥})))
13	12	fveq2d 6778	. . 3 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))))
14		esumeq1 32002	. . 3 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))
15	13, 14	eqeq12d 2754	. 2 ⊢ (𝑎 = (𝑏 ∪ {𝑥}) → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))))
16		unieq 4850	. . . . 5 ⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴)
17	16	ineq2d 4146	. . . 4 ⊢ (𝑎 = 𝐴 → (𝐸 ∩ ∪ 𝑎) = (𝐸 ∩ ∪ 𝐴))
18	17	fveq2d 6778	. . 3 ⊢ (𝑎 = 𝐴 → (𝑀‘(𝐸 ∩ ∪ 𝑎)) = (𝑀‘(𝐸 ∩ ∪ 𝐴)))
19		esumeq1 32002	. . 3 ⊢ (𝑎 = 𝐴 → Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) = Σ^𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))
20	18, 19	eqeq12d 2754	. 2 ⊢ (𝑎 = 𝐴 → ((𝑀‘(𝐸 ∩ ∪ 𝑎)) = Σ^𝑦 ∈ 𝑎(𝑀‘(𝐸 ∩ 𝑦)) ↔ (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ^𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦))))
21		carsgsiga.1	. . 3 ⊢ (𝜑 → (𝑀‘∅) = 0)
22		uni0 4869	. . . . . 6 ⊢ ∪ ∅ = ∅
23	22	ineq2i 4143	. . . . 5 ⊢ (𝐸 ∩ ∪ ∅) = (𝐸 ∩ ∅)
24		in0 4325	. . . . 5 ⊢ (𝐸 ∩ ∅) = ∅
25	23, 24	eqtri 2766	. . . 4 ⊢ (𝐸 ∩ ∪ ∅) = ∅
26	25	fveq2i 6777	. . 3 ⊢ (𝑀‘(𝐸 ∩ ∪ ∅)) = (𝑀‘∅)
27		esumnul 32016	. . 3 ⊢ Σ^*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)) = 0
28	21, 26, 27	3eqtr4g 2803	. 2 ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ ∅)) = Σ^*𝑦 ∈ ∅(𝑀‘(𝐸 ∩ 𝑦)))
29		simpr 485	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)))
30	29	eqcomd 2744	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
31		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
32	31	ineq2d 4146	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝐸 ∩ 𝑦) = (𝐸 ∩ 𝑥))
33	32	fveq2d 6778	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 = 𝑥) → (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
34		simprr 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑥 ∈ (𝐴 ∖ 𝑏))
35		carsgval.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))
36	35	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
37		carsgclctunlem1.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂)
38	37	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝐸 ∈ 𝒫 𝑂)
39	38	elpwincl1 30874	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ 𝑥) ∈ 𝒫 𝑂)
40	36, 39	ffvelrnd 6962	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘(𝐸 ∩ 𝑥)) ∈ (0[,]+∞))
41	33, 34, 40	esumsn 32033	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
42	41	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝑥)))
43	30, 42	oveq12d 7293	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
44		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏)))
45		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑦𝑏
46		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑦{𝑥}
47		vex 3436	. . . . . . 7 ⊢ 𝑏 ∈ V
48	47	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ∈ V)
49		snex 5354	. . . . . . 7 ⊢ {𝑥} ∈ V
50	49	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → {𝑥} ∈ V)
51	34	eldifbd 3900	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ¬ 𝑥 ∈ 𝑏)
52		disjsn 4647	. . . . . . 7 ⊢ ((𝑏 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝑏)
53	51, 52	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑏 ∩ {𝑥}) = ∅)
54	35	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
55	37	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → 𝐸 ∈ 𝒫 𝑂)
56	55	elpwincl1 30874	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂)
57	54, 56	ffvelrnd 6962	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ 𝑏) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞))
58	35	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
59	37	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → 𝐸 ∈ 𝒫 𝑂)
60	59	elpwincl1 30874	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝐸 ∩ 𝑦) ∈ 𝒫 𝑂)
61	58, 60	ffvelrnd 6962	. . . . . 6 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑦 ∈ {𝑥}) → (𝑀‘(𝐸 ∩ 𝑦)) ∈ (0[,]+∞))
62	44, 45, 46, 48, 50, 53, 57, 61	esumsplit 32021	. . . . 5 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^*𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))))
63	62	adantr 481	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)) = (Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) +_𝑒 Σ^𝑦 ∈ {𝑥} (𝑀‘(𝐸 ∩ 𝑦))))
64		uniun 4864	. . . . . . . 8 ⊢ ∪ (𝑏 ∪ {𝑥}) = (∪ 𝑏 ∪ ∪ {𝑥})
65		vex 3436	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
66	65	unisn 4861	. . . . . . . . 9 ⊢ ∪ {𝑥} = 𝑥
67	66	uneq2i 4094	. . . . . . . 8 ⊢ (∪ 𝑏 ∪ ∪ {𝑥}) = (∪ 𝑏 ∪ 𝑥)
68	64, 67	eqtri 2766	. . . . . . 7 ⊢ ∪ (𝑏 ∪ {𝑥}) = (∪ 𝑏 ∪ 𝑥)
69	68	ineq2i 4143	. . . . . 6 ⊢ (𝐸 ∩ ∪ (𝑏 ∪ {𝑥})) = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))
70	69	fveq2i 6777	. . . . 5 ⊢ (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))
71		inass 4153	. . . . . . . . . 10 ⊢ ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏) = (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏))
72		indir 4209	. . . . . . . . . . . 12 ⊢ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏) = ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏))
73		inidm 4152	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑏 ∩ ∪ 𝑏) = ∪ 𝑏
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪ 𝑏 ∩ ∪ 𝑏) = ∪ 𝑏)
75		incom 4135	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑏 ∩ 𝑥) = (𝑥 ∩ ∪ 𝑏)
76		carsgclctunlem1.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦)
77	76	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → Disj 𝑦 ∈ 𝐴 𝑦)
78		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ 𝐴)
79	78	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → 𝑏 ⊆ 𝐴)
80	77, 79, 34	disjuniel 30936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∪ 𝑏 ∩ 𝑥) = ∅)
81	75, 80	eqtr3id 2792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑥 ∩ ∪ 𝑏) = ∅)
82	74, 81	uneq12d 4098	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏)) = (∪ 𝑏 ∪ ∅))
83		un0 4324	. . . . . . . . . . . . 13 ⊢ (∪ 𝑏 ∪ ∅) = ∪ 𝑏
84	82, 83	eqtrdi 2794	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∩ ∪ 𝑏) ∪ (𝑥 ∩ ∪ 𝑏)) = ∪ 𝑏)
85	72, 84	eqtrid 2790	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏) = ∪ 𝑏)
86	85	ineq2d 4146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∩ ∪ 𝑏)) = (𝐸 ∩ ∪ 𝑏))
87	71, 86	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏) = (𝐸 ∩ ∪ 𝑏))
88	87	fveq2d 6778	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ ∪ 𝑏)))
89		indif2 4204	. . . . . . . . . 10 ⊢ (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏)) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)
90		uncom 4087	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑏 ∪ 𝑥) = (𝑥 ∪ ∪ 𝑏)
91	90	difeq1i 4053	. . . . . . . . . . . . 13 ⊢ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏)
92		difun2 4414	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏) = (𝑥 ∖ ∪ 𝑏)
93		disj3 4387	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ ↔ 𝑥 = (𝑥 ∖ ∪ 𝑏))
94	93	biimpi 215	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → 𝑥 = (𝑥 ∖ ∪ 𝑏))
95	92, 94	eqtr4id 2797	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → ((𝑥 ∪ ∪ 𝑏) ∖ ∪ 𝑏) = 𝑥)
96	91, 95	eqtrid 2790	. . . . . . . . . . . 12 ⊢ ((𝑥 ∩ ∪ 𝑏) = ∅ → ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥)
97	81, 96	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏) = 𝑥)
98	97	ineq2d 4146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ ((∪ 𝑏 ∪ 𝑥) ∖ ∪ 𝑏)) = (𝐸 ∩ 𝑥))
99	89, 98	eqtr3id 2792	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏) = (𝐸 ∩ 𝑥))
100	99	fveq2d 6778	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)) = (𝑀‘(𝐸 ∩ 𝑥)))
101	88, 100	oveq12d 7293	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
102		carsgval.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ 𝑉)
103	102	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑂 ∈ 𝑉)
104	35	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
105	21	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (𝑀‘∅) = 0)
106		carsgsiga.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ^*𝑦 ∈ 𝑥(𝑀‘𝑦))
107	106	3adant1r 1176	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ^*𝑦 ∈ 𝑥(𝑀‘𝑦))
108		fiunelcarsg.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ Fin)
109		ssfi 8956	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin)
110	108, 109	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin)
111		fiunelcarsg.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))
112	111	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝐴 ⊆ (toCaraSiga‘𝑀))
113	78, 112	sstrd 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ (toCaraSiga‘𝑀))
114	103, 104, 105, 107, 110, 113	fiunelcarsg 32283	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∪ 𝑏 ∈ (toCaraSiga‘𝑀))
115	102, 35	elcarsg 32272	. . . . . . . . . . . 12 ⊢ (𝜑 → (∪ 𝑏 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))))
116	115	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))))
117	114, 116	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (∪ 𝑏 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒)))
118	117	simprd 496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))
119	118	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒))
120	38	elpwincl1 30874	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∈ 𝒫 𝑂)
121		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))
122	121	ineq1d 4145	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∩ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏))
123	122	fveq2d 6778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∩ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)))
124	121	difeq1d 4056	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑒 ∖ ∪ 𝑏) = ((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))
125	124	fveq2d 6778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘(𝑒 ∖ ∪ 𝑏)) = (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏)))
126	123, 125	oveq12d 7293	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → ((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))))
127	121	fveq2d 6778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (𝑀‘𝑒) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
128	126, 127	eqeq12d 2754	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ 𝑒 = (𝐸 ∩ (∪ 𝑏 ∪ 𝑥))) → (((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) ↔ ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))))
129	120, 128	rspcdv 3553	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝑒 ∖ ∪ 𝑏))) = (𝑀‘𝑒) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥)))))
130	119, 129	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∩ ∪ 𝑏)) +_𝑒 (𝑀‘((𝐸 ∩ (∪ 𝑏 ∪ 𝑥)) ∖ ∪ 𝑏))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
131	101, 130	eqtr3d 2780	. . . . . 6 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
132	131	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))) = (𝑀‘(𝐸 ∩ (∪ 𝑏 ∪ 𝑥))))
133	70, 132	eqtr4id 2797	. . . 4 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^*𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = ((𝑀‘(𝐸 ∩ ∪ 𝑏)) +_𝑒 (𝑀‘(𝐸 ∩ 𝑥))))
134	43, 63, 133	3eqtr4rd 2789	. . 3 ⊢ (((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) ∧ (𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦))) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦)))
135	134	ex 413	. 2 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ (𝐴 ∖ 𝑏))) → ((𝑀‘(𝐸 ∩ ∪ 𝑏)) = Σ^𝑦 ∈ 𝑏(𝑀‘(𝐸 ∩ 𝑦)) → (𝑀‘(𝐸 ∩ ∪ (𝑏 ∪ {𝑥}))) = Σ^𝑦 ∈ (𝑏 ∪ {𝑥})(𝑀‘(𝐸 ∩ 𝑦))))
136	5, 10, 15, 20, 28, 135, 108	findcard2d 8949	1 ⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = Σ^*𝑦 ∈ 𝐴(𝑀‘(𝐸 ∩ 𝑦)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 𝒫 cpw 4533 {csn 4561 ∪ cuni 4839 Disj wdisj 5039 class class class wbr 5074 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ωcom 7712 ≼ cdom 8731 Fincfn 8733 0cc0 10871 +∞cpnf 11006 ≤ cle 11010 +_𝑒 cxad 12846 [,]cicc 13082 Σ^*cesum 31995 toCaraSigaccarsg 32268

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-disj 5040 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-pm 8618 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-fac 13988 df-bc 14017 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398 df-ef 15777 df-sin 15779 df-cos 15780 df-pi 15782 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-hom 16986 df-cco 16987 df-rest 17133 df-topn 17134 df-0g 17152 df-gsum 17153 df-topgen 17154 df-pt 17155 df-prds 17158 df-ordt 17212 df-xrs 17213 df-qtop 17218 df-imas 17219 df-xps 17221 df-mre 17295 df-mrc 17296 df-acs 17298 df-ps 18284 df-tsr 18285 df-plusf 18325 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-mhm 18430 df-submnd 18431 df-grp 18580 df-minusg 18581 df-sbg 18582 df-mulg 18701 df-subg 18752 df-cntz 18923 df-cmn 19388 df-abl 19389 df-mgp 19721 df-ur 19738 df-ring 19785 df-cring 19786 df-subrg 20022 df-abv 20077 df-lmod 20125 df-scaf 20126 df-sra 20434 df-rgmod 20435 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-haus 22466 df-tx 22713 df-hmeo 22906 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-tmd 23223 df-tgp 23224 df-tsms 23278 df-trg 23311 df-xms 23473 df-ms 23474 df-tms 23475 df-nm 23738 df-ngp 23739 df-nrg 23741 df-nlm 23742 df-ii 24040 df-cncf 24041 df-limc 25030 df-dv 25031 df-log 25712 df-esum 31996 df-carsg 32269

This theorem is referenced by: carsggect 32285 carsgclctunlem2 32286

W3C validator