pmeasmono

Description: This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Hypotheses	caraext.1	$⊢ φ \to P : R ⟶ [0, +∞]$
	caraext.2	$⊢ φ \to P (\emptyset) = 0$
	caraext.3	$⊢ (φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{*}} P (y)$
	pmeasmono.1	$⊢ φ \to A \in R$
	pmeasmono.2	$⊢ φ \to B \in R$
	pmeasmono.3	$⊢ φ \to B ∖ A \in R$
	pmeasmono.4	$⊢ φ \to A \subseteq B$
Assertion	pmeasmono	$⊢ φ \to P (A) \leq P (B)$

Proof

Step	Hyp	Ref	Expression
1		caraext.1	$⊢ φ \to P : R ⟶ [0, +∞]$
2		caraext.2	$⊢ φ \to P (\emptyset) = 0$
3		caraext.3	$⊢ (φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{*}} P (y)$
4		pmeasmono.1	$⊢ φ \to A \in R$
5		pmeasmono.2	$⊢ φ \to B \in R$
6		pmeasmono.3	$⊢ φ \to B ∖ A \in R$
7		pmeasmono.4	$⊢ φ \to A \subseteq B$
8		eqimss	$⊢ A = B ∖ A \to A \subseteq B ∖ A$
9		ssdifeq0	$⊢ A \subseteq B ∖ A \leftrightarrow A = \emptyset$
10	8 9	sylib	$⊢ A = B ∖ A \to A = \emptyset$
11	10	fveq2d	$⊢ A = B ∖ A \to P (A) = P (\emptyset)$
12	11	adantl	$⊢ (φ \land A = B ∖ A) \to P (A) = P (\emptyset)$
13	2	adantr	$⊢ (φ \land A = B ∖ A) \to P (\emptyset) = 0$
14	12 13	eqtrd	$⊢ (φ \land A = B ∖ A) \to P (A) = 0$
15	1 5	ffvelcdmd	$⊢ φ \to P (B) \in [0, +∞]$
16		elxrge0	$⊢ P (B) \in [0, +∞] \leftrightarrow (P (B) \in ℝ^{*} \land 0 \leq P (B))$
17	16	simprbi	$⊢ P (B) \in [0, +∞] \to 0 \leq P (B)$
18	15 17	syl	$⊢ φ \to 0 \leq P (B)$
19	18	adantr	$⊢ (φ \land A = B ∖ A) \to 0 \leq P (B)$
20	14 19	eqbrtrd	$⊢ (φ \land A = B ∖ A) \to P (A) \leq P (B)$
21		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
22	1	adantr	$⊢ (φ \land A \neq B ∖ A) \to P : R ⟶ [0, +∞]$
23	4	adantr	$⊢ (φ \land A \neq B ∖ A) \to A \in R$
24	22 23	ffvelcdmd	$⊢ (φ \land A \neq B ∖ A) \to P (A) \in [0, +∞]$
25	21 24	sselid	$⊢ (φ \land A \neq B ∖ A) \to P (A) \in ℝ^{*}$
26	6	adantr	$⊢ (φ \land A \neq B ∖ A) \to B ∖ A \in R$
27	22 26	ffvelcdmd	$⊢ (φ \land A \neq B ∖ A) \to P (B ∖ A) \in [0, +∞]$
28		xrge0addge	$⊢ (P (A) \in ℝ^{*} \land P (B ∖ A) \in [0, +∞]) \to P (A) \leq P (A) +_{𝑒} P (B ∖ A)$
29	25 27 28	syl2anc	$⊢ (φ \land A \neq B ∖ A) \to P (A) \leq P (A) +_{𝑒} P (B ∖ A)$
30		prct	$⊢ (A \in R \land B ∖ A \in R) \to \{A, B ∖ A\} ≼ ω$
31	4 6 30	syl2anc	$⊢ φ \to \{A, B ∖ A\} ≼ ω$
32	31	adantr	$⊢ (φ \land A \neq B ∖ A) \to \{A, B ∖ A\} ≼ ω$
33		prssi	$⊢ (A \in R \land B ∖ A \in R) \to \{A, B ∖ A\} \subseteq R$
34	4 6 33	syl2anc	$⊢ φ \to \{A, B ∖ A\} \subseteq R$
35	34	adantr	$⊢ (φ \land A \neq B ∖ A) \to \{A, B ∖ A\} \subseteq R$
36		disjdif	$⊢ A \cap (B ∖ A) = \emptyset$
37		simpr	$⊢ (φ \land A \neq B ∖ A) \to A \neq B ∖ A$
38		id	$⊢ y = A \to y = A$
39		id	$⊢ y = B ∖ A \to y = B ∖ A$
40	38 39	disjprg	$⊢ (A \in R \land B ∖ A \in R \land A \neq B ∖ A) \to (\underset{y \in \{A, B ∖ A\}}{Disj} y \leftrightarrow A \cap (B ∖ A) = \emptyset)$
41	23 26 37 40	syl3anc	$⊢ (φ \land A \neq B ∖ A) \to (\underset{y \in \{A, B ∖ A\}}{Disj} y \leftrightarrow A \cap (B ∖ A) = \emptyset)$
42	36 41	mpbiri	$⊢ (φ \land A \neq B ∖ A) \to \underset{y \in \{A, B ∖ A\}}{Disj} y$
43	32 35 42	3jca	$⊢ (φ \land A \neq B ∖ A) \to (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)$
44		prex	$⊢ \{A, B ∖ A\} \in V$
45		biidd	$⊢ x = \{A, B ∖ A\} \to (φ \leftrightarrow φ)$
46		breq1	$⊢ x = \{A, B ∖ A\} \to (x ≼ ω \leftrightarrow \{A, B ∖ A\} ≼ ω)$
47		sseq1	$⊢ x = \{A, B ∖ A\} \to (x \subseteq R \leftrightarrow \{A, B ∖ A\} \subseteq R)$
48		disjeq1	$⊢ x = \{A, B ∖ A\} \to (\underset{y \in x}{Disj} y \leftrightarrow \underset{y \in \{A, B ∖ A\}}{Disj} y)$
49	46 47 48	3anbi123d	$⊢ x = \{A, B ∖ A\} \to ((x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y) \leftrightarrow (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y))$
50	45 49	anbi12d	$⊢ x = \{A, B ∖ A\} \to ((φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \leftrightarrow (φ \land (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)))$
51		unieq	$⊢ x = \{A, B ∖ A\} \to ⋃ x = ⋃ \{A, B ∖ A\}$
52	51	fveq2d	$⊢ x = \{A, B ∖ A\} \to P (⋃ x) = P (⋃ \{A, B ∖ A\})$
53		esumeq1	$⊢ x = \{A, B ∖ A\} \to \underset{y \in x}{\sum^{}} P (y) = \underset{y \in \{A, B ∖ A\}}{\sum^{}} P (y)$
54	52 53	eqeq12d	$⊢ x = \{A, B ∖ A\} \to (P (⋃ x) = \underset{y \in x}{\sum^{}} P (y) \leftrightarrow P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{}} P (y))$
55	50 54	imbi12d	$⊢ x = \{A, B ∖ A\} \to (((φ \land (x ≼ ω \land x \subseteq R \land \underset{y \in x}{Disj} y)) \to P (⋃ x) = \underset{y \in x}{\sum^{}} P (y)) \leftrightarrow ((φ \land (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)) \to P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{}} P (y)))$
56	55 3	vtoclg	$⊢ \{A, B ∖ A\} \in V \to ((φ \land (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)) \to P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{*}} P (y))$
57	44 56	ax-mp	$⊢ (φ \land (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)) \to P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{*}} P (y)$
58	57	adantlr	$⊢ ((φ \land A \neq B ∖ A) \land (\{A, B ∖ A\} ≼ ω \land \{A, B ∖ A\} \subseteq R \land \underset{y \in \{A, B ∖ A\}}{Disj} y)) \to P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{*}} P (y)$
59	43 58	mpdan	$⊢ (φ \land A \neq B ∖ A) \to P (⋃ \{A, B ∖ A\}) = \underset{y \in \{A, B ∖ A\}}{\sum^{*}} P (y)$
60		uniprg	$⊢ (A \in R \land B ∖ A \in R) \to ⋃ \{A, B ∖ A\} = A \cup (B ∖ A)$
61	4 6 60	syl2anc	$⊢ φ \to ⋃ \{A, B ∖ A\} = A \cup (B ∖ A)$
62		undif	$⊢ A \subseteq B \leftrightarrow A \cup (B ∖ A) = B$
63	7 62	sylib	$⊢ φ \to A \cup (B ∖ A) = B$
64	61 63	eqtrd	$⊢ φ \to ⋃ \{A, B ∖ A\} = B$
65	64	adantr	$⊢ (φ \land A \neq B ∖ A) \to ⋃ \{A, B ∖ A\} = B$
66	65	fveq2d	$⊢ (φ \land A \neq B ∖ A) \to P (⋃ \{A, B ∖ A\}) = P (B)$
67		simpr	$⊢ ((φ \land A \neq B ∖ A) \land y = A) \to y = A$
68	67	fveq2d	$⊢ ((φ \land A \neq B ∖ A) \land y = A) \to P (y) = P (A)$
69		simpr	$⊢ ((φ \land A \neq B ∖ A) \land y = B ∖ A) \to y = B ∖ A$
70	69	fveq2d	$⊢ ((φ \land A \neq B ∖ A) \land y = B ∖ A) \to P (y) = P (B ∖ A)$
71	68 70 23 26 24 27 37	esumpr	$⊢ (φ \land A \neq B ∖ A) \to \underset{y \in \{A, B ∖ A\}}{\sum^{*}} P (y) = P (A) +_{𝑒} P (B ∖ A)$
72	59 66 71	3eqtr3d	$⊢ (φ \land A \neq B ∖ A) \to P (B) = P (A) +_{𝑒} P (B ∖ A)$
73	29 72	breqtrrd	$⊢ (φ \land A \neq B ∖ A) \to P (A) \leq P (B)$
74	20 73	pm2.61dane	$⊢ φ \to P (A) \leq P (B)$

Metamath Proof Explorer

Theorem pmeasmono

Proof