carsgsigalem

Description: Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	$⊢ φ \to O \in V$
	carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
	carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
	carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
Assertion	carsgsigalem	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$⊢ φ \to O \in V$
2		carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
3		carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
4		carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
5		simpr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to e = f$
6	5	uneq2d	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to e \cup e = e \cup f$
7		unidm	$⊢ e \cup e = e$
8	6 7	eqtr3di	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to e \cup f = e$
9	8	fveq2d	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (e \cup f) = M (e)$
10		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
11		simp1	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to φ$
12	11 2	syl	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M : 𝒫 O ⟶ [0, +∞]$
13		simp2	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to e \in 𝒫 O$
14	12 13	ffvelrnd	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e) \in [0, +∞]$
15	10 14	sselid	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e) \in ℝ^{*}$
16	15	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (e) \in ℝ^{*}$
17	5	fveq2d	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (e) = M (f)$
18	17 16	eqeltrrd	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (f) \in ℝ^{*}$
19		simp3	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to f \in 𝒫 O$
20	12 19	ffvelrnd	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (f) \in [0, +∞]$
21	20	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (f) \in [0, +∞]$
22		elxrge0	$⊢ M (f) \in [0, +∞] \leftrightarrow (M (f) \in ℝ^{*} \land 0 \leq M (f))$
23	22	simprbi	$⊢ M (f) \in [0, +∞] \to 0 \leq M (f)$
24	21 23	syl	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to 0 \leq M (f)$
25		xraddge02	$⊢ (M (e) \in ℝ^{} \land M (f) \in ℝ^{}) \to (0 \leq M (f) \to M (e) \leq M (e) +_{𝑒} M (f))$
26	25	imp	$⊢ ((M (e) \in ℝ^{} \land M (f) \in ℝ^{}) \land 0 \leq M (f)) \to M (e) \leq M (e) +_{𝑒} M (f)$
27	16 18 24 26	syl21anc	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (e) \leq M (e) +_{𝑒} M (f)$
28	9 27	eqbrtrd	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e = f) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$
29		uniprg	$⊢ (e \in 𝒫 O \land f \in 𝒫 O) \to ⋃ \{e, f\} = e \cup f$
30	29	fveq2d	$⊢ (e \in 𝒫 O \land f \in 𝒫 O) \to M (⋃ \{e, f\}) = M (e \cup f)$
31	30	3adant1	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (⋃ \{e, f\}) = M (e \cup f)$
32		prct	$⊢ (e \in 𝒫 O \land f \in 𝒫 O) \to \{e, f\} ≼ ω$
33	32	3adant1	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to \{e, f\} ≼ ω$
34		prssi	$⊢ (e \in 𝒫 O \land f \in 𝒫 O) \to \{e, f\} \subseteq 𝒫 O$
35	34	3adant1	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to \{e, f\} \subseteq 𝒫 O$
36		prex	$⊢ \{e, f\} \in V$
37		breq1	$⊢ x = \{e, f\} \to (x ≼ ω \leftrightarrow \{e, f\} ≼ ω)$
38		sseq1	$⊢ x = \{e, f\} \to (x \subseteq 𝒫 O \leftrightarrow \{e, f\} \subseteq 𝒫 O)$
39	37 38	3anbi23d	$⊢ x = \{e, f\} \to ((φ \land x ≼ ω \land x \subseteq 𝒫 O) \leftrightarrow (φ \land \{e, f\} ≼ ω \land \{e, f\} \subseteq 𝒫 O))$
40		unieq	$⊢ x = \{e, f\} \to ⋃ x = ⋃ \{e, f\}$
41	40	fveq2d	$⊢ x = \{e, f\} \to M (⋃ x) = M (⋃ \{e, f\})$
42		esumeq1	$⊢ x = \{e, f\} \to \underset{y \in x}{\sum^{}} M (y) = \underset{y \in \{e, f\}}{\sum^{}} M (y)$
43	41 42	breq12d	$⊢ x = \{e, f\} \to (M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y) \leftrightarrow M (⋃ \{e, f\}) \leq \underset{y \in \{e, f\}}{\sum^{}} M (y))$
44	39 43	imbi12d	$⊢ x = \{e, f\} \to (((φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y)) \leftrightarrow ((φ \land \{e, f\} ≼ ω \land \{e, f\} \subseteq 𝒫 O) \to M (⋃ \{e, f\}) \leq \underset{y \in \{e, f\}}{\sum^{}} M (y)))$
45	44 4	vtoclg	$⊢ \{e, f\} \in V \to ((φ \land \{e, f\} ≼ ω \land \{e, f\} \subseteq 𝒫 O) \to M (⋃ \{e, f\}) \leq \underset{y \in \{e, f\}}{\sum^{*}} M (y))$
46	36 45	ax-mp	$⊢ (φ \land \{e, f\} ≼ ω \land \{e, f\} \subseteq 𝒫 O) \to M (⋃ \{e, f\}) \leq \underset{y \in \{e, f\}}{\sum^{*}} M (y)$
47	11 33 35 46	syl3anc	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (⋃ \{e, f\}) \leq \underset{y \in \{e, f\}}{\sum^{*}} M (y)$
48	31 47	eqbrtrrd	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e \cup f) \leq \underset{y \in \{e, f\}}{\sum^{*}} M (y)$
49	48	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to M (e \cup f) \leq \underset{y \in \{e, f\}}{\sum^{*}} M (y)$
50		simpr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land y = e) \to y = e$
51	50	fveq2d	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land y = e) \to M (y) = M (e)$
52	51	adantlr	$⊢ (((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \land y = e) \to M (y) = M (e)$
53		simpr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land y = f) \to y = f$
54	53	fveq2d	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land y = f) \to M (y) = M (f)$
55	54	adantlr	$⊢ (((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \land y = f) \to M (y) = M (f)$
56	13	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to e \in 𝒫 O$
57	19	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to f \in 𝒫 O$
58	14	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to M (e) \in [0, +∞]$
59	20	adantr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to M (f) \in [0, +∞]$
60		simpr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to e \neq f$
61	52 55 56 57 58 59 60	esumpr	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to \underset{y \in \{e, f\}}{\sum^{*}} M (y) = M (e) +_{𝑒} M (f)$
62	49 61	breqtrd	$⊢ ((φ \land e \in 𝒫 O \land f \in 𝒫 O) \land e \neq f) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$
63	28 62	pm2.61dane	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$

Metamath Proof Explorer

Theorem carsgsigalem

Proof