carsgclctunlem1

	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)$
	fiunelcarsg.1	$⊢ φ \to A \in Fin$
	fiunelcarsg.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
	carsgclctunlem1.1	$⊢ φ \to \underset{y \in A}{Disj} y$
	carsgclctunlem1.2	$⊢ φ \to E \in 𝒫 O$
Assertion	carsgclctunlem1	$⊢ φ \to M (E \cap ⋃ A) = \underset{y \in A}{\sum^{*}} M (E \cap y)$

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		fiunelcarsg.1	$⊢ φ \to A \in Fin$
6		fiunelcarsg.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
7		carsgclctunlem1.1	$⊢ φ \to \underset{y \in A}{Disj} y$
8		carsgclctunlem1.2	$⊢ φ \to E \in 𝒫 O$
9		unieq	$⊢ a = \emptyset \to ⋃ a = ⋃ \emptyset$
10	9	ineq2d	$⊢ a = \emptyset \to E \cap ⋃ a = E \cap ⋃ \emptyset$
11	10	fveq2d	$⊢ a = \emptyset \to M (E \cap ⋃ a) = M (E \cap ⋃ \emptyset)$
12		esumeq1	$⊢ a = \emptyset \to \underset{y \in a}{\sum^{}} M (E \cap y) = \underset{y \in \emptyset}{\sum^{}} M (E \cap y)$
13	11 12	eqeq12d	$⊢ a = \emptyset \to (M (E \cap ⋃ a) = \underset{y \in a}{\sum^{}} M (E \cap y) \leftrightarrow M (E \cap ⋃ \emptyset) = \underset{y \in \emptyset}{\sum^{}} M (E \cap y))$
14		unieq	$⊢ a = b \to ⋃ a = ⋃ b$
15	14	ineq2d	$⊢ a = b \to E \cap ⋃ a = E \cap ⋃ b$
16	15	fveq2d	$⊢ a = b \to M (E \cap ⋃ a) = M (E \cap ⋃ b)$
17		esumeq1	$⊢ a = b \to \underset{y \in a}{\sum^{}} M (E \cap y) = \underset{y \in b}{\sum^{}} M (E \cap y)$
18	16 17	eqeq12d	$⊢ a = b \to (M (E \cap ⋃ a) = \underset{y \in a}{\sum^{}} M (E \cap y) \leftrightarrow M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y))$
19		unieq	$⊢ a = b \cup \{x\} \to ⋃ a = ⋃ (b \cup \{x\})$
20	19	ineq2d	$⊢ a = b \cup \{x\} \to E \cap ⋃ a = E \cap ⋃ (b \cup \{x\})$
21	20	fveq2d	$⊢ a = b \cup \{x\} \to M (E \cap ⋃ a) = M (E \cap ⋃ (b \cup \{x\}))$
22		esumeq1	$⊢ a = b \cup \{x\} \to \underset{y \in a}{\sum^{}} M (E \cap y) = \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y)$
23	21 22	eqeq12d	$⊢ a = b \cup \{x\} \to (M (E \cap ⋃ a) = \underset{y \in a}{\sum^{}} M (E \cap y) \leftrightarrow M (E \cap ⋃ (b \cup \{x\})) = \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y))$
24		unieq	$⊢ a = A \to ⋃ a = ⋃ A$
25	24	ineq2d	$⊢ a = A \to E \cap ⋃ a = E \cap ⋃ A$
26	25	fveq2d	$⊢ a = A \to M (E \cap ⋃ a) = M (E \cap ⋃ A)$
27		esumeq1	$⊢ a = A \to \underset{y \in a}{\sum^{}} M (E \cap y) = \underset{y \in A}{\sum^{}} M (E \cap y)$
28	26 27	eqeq12d	$⊢ a = A \to (M (E \cap ⋃ a) = \underset{y \in a}{\sum^{}} M (E \cap y) \leftrightarrow M (E \cap ⋃ A) = \underset{y \in A}{\sum^{}} M (E \cap y))$
29		uni0	$⊢ ⋃ \emptyset = \emptyset$
30	29	ineq2i	$⊢ E \cap ⋃ \emptyset = E \cap \emptyset$
31		in0	$⊢ E \cap \emptyset = \emptyset$
32	30 31	eqtri	$⊢ E \cap ⋃ \emptyset = \emptyset$
33	32	fveq2i	$⊢ M (E \cap ⋃ \emptyset) = M (\emptyset)$
34		esumnul	$⊢ \underset{y \in \emptyset}{\sum^{*}} M (E \cap y) = 0$
35	3 33 34	3eqtr4g	$⊢ φ \to M (E \cap ⋃ \emptyset) = \underset{y \in \emptyset}{\sum^{*}} M (E \cap y)$
36		simpr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)$
37	36	eqcomd	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to \underset{y \in b}{\sum^{}} M (E \cap y) = M (E \cap ⋃ b)$
38		simpr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y = x) \to y = x$
39	38	ineq2d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y = x) \to E \cap y = E \cap x$
40	39	fveq2d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y = x) \to M (E \cap y) = M (E \cap x)$
41		simprr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to x \in (A ∖ b)$
42	2	adantr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M : 𝒫 O ⟶ [0, +∞]$
43	8	adantr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \in 𝒫 O$
44	43	elpwincl1	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap x \in 𝒫 O$
45	42 44	ffvelcdmd	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M (E \cap x) \in [0, +∞]$
46	40 41 45	esumsn	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \underset{y \in \{x\}}{\sum^{*}} M (E \cap y) = M (E \cap x)$
47	46	adantr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to \underset{y \in \{x\}}{\sum^{}} M (E \cap y) = M (E \cap x)$
48	37 47	oveq12d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to \underset{y \in b}{\sum^{}} M (E \cap y) +_{𝑒} \underset{y \in \{x\}}{\sum^{*}} M (E \cap y) = M (E \cap ⋃ b) +_{𝑒} M (E \cap x)$
49		nfv	$⊢ Ⅎ y (φ \land (b \subseteq A \land x \in (A ∖ b)))$
50		nfcv	$⊢ \underline{Ⅎ} y b$
51		nfcv	$⊢ \underline{Ⅎ} y \{x\}$
52		vex	$⊢ b \in V$
53	52	a1i	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to b \in V$
54		vsnex	$⊢ \{x\} \in V$
55	54	a1i	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \{x\} \in V$
56	41	eldifbd	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \neg x \in b$
57		disjsn	$⊢ b \cap \{x\} = \emptyset \leftrightarrow \neg x \in b$
58	56 57	sylibr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to b \cap \{x\} = \emptyset$
59	2	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in b) \to M : 𝒫 O ⟶ [0, +∞]$
60	8	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in b) \to E \in 𝒫 O$
61	60	elpwincl1	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in b) \to E \cap y \in 𝒫 O$
62	59 61	ffvelcdmd	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in b) \to M (E \cap y) \in [0, +∞]$
63	2	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in \{x\}) \to M : 𝒫 O ⟶ [0, +∞]$
64	8	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in \{x\}) \to E \in 𝒫 O$
65	64	elpwincl1	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in \{x\}) \to E \cap y \in 𝒫 O$
66	63 65	ffvelcdmd	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land y \in \{x\}) \to M (E \cap y) \in [0, +∞]$
67	49 50 51 53 55 58 62 66	esumsplit	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y) = \underset{y \in b}{\sum^{}} M (E \cap y) +_{𝑒} \underset{y \in \{x\}}{\sum^{*}} M (E \cap y)$
68	67	adantr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y) = \underset{y \in b}{\sum^{}} M (E \cap y) +_{𝑒} \underset{y \in \{x\}}{\sum^{}} M (E \cap y)$
69		uniun	$⊢ ⋃ (b \cup \{x\}) = ⋃ b \cup ⋃ \{x\}$
70		unisnv	$⊢ ⋃ \{x\} = x$
71	70	uneq2i	$⊢ ⋃ b \cup ⋃ \{x\} = ⋃ b \cup x$
72	69 71	eqtri	$⊢ ⋃ (b \cup \{x\}) = ⋃ b \cup x$
73	72	ineq2i	$⊢ E \cap ⋃ (b \cup \{x\}) = E \cap (⋃ b \cup x)$
74	73	fveq2i	$⊢ M (E \cap ⋃ (b \cup \{x\})) = M (E \cap (⋃ b \cup x))$
75		inass	$⊢ (E \cap (⋃ b \cup x)) \cap ⋃ b = E \cap ((⋃ b \cup x) \cap ⋃ b)$
76		indir	$⊢ (⋃ b \cup x) \cap ⋃ b = (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b)$
77		inidm	$⊢ ⋃ b \cap ⋃ b = ⋃ b$
78	77	a1i	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to ⋃ b \cap ⋃ b = ⋃ b$
79		incom	$⊢ ⋃ b \cap x = x \cap ⋃ b$
80	7	adantr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \underset{y \in A}{Disj} y$
81		simpr	$⊢ (φ \land b \subseteq A) \to b \subseteq A$
82	81	adantrr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to b \subseteq A$
83	80 82 41	disjuniel	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to ⋃ b \cap x = \emptyset$
84	79 83	eqtr3id	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to x \cap ⋃ b = \emptyset$
85	78 84	uneq12d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b) = ⋃ b \cup \emptyset$
86		un0	$⊢ ⋃ b \cup \emptyset = ⋃ b$
87	85 86	eqtrdi	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b) = ⋃ b$
88	76 87	eqtrid	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cup x) \cap ⋃ b = ⋃ b$
89	88	ineq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap ((⋃ b \cup x) \cap ⋃ b) = E \cap ⋃ b$
90	75 89	eqtrid	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (E \cap (⋃ b \cup x)) \cap ⋃ b = E \cap ⋃ b$
91	90	fveq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) \cap ⋃ b) = M (E \cap ⋃ b)$
92		indif2	$⊢ E \cap ((⋃ b \cup x) ∖ ⋃ b) = (E \cap (⋃ b \cup x)) ∖ ⋃ b$
93		uncom	$⊢ ⋃ b \cup x = x \cup ⋃ b$
94	93	difeq1i	$⊢ (⋃ b \cup x) ∖ ⋃ b = (x \cup ⋃ b) ∖ ⋃ b$
95		difun2	$⊢ (x \cup ⋃ b) ∖ ⋃ b = x ∖ ⋃ b$
96		disj3	$⊢ x \cap ⋃ b = \emptyset \leftrightarrow x = x ∖ ⋃ b$
97	96	biimpi	$⊢ x \cap ⋃ b = \emptyset \to x = x ∖ ⋃ b$
98	95 97	eqtr4id	$⊢ x \cap ⋃ b = \emptyset \to (x \cup ⋃ b) ∖ ⋃ b = x$
99	94 98	eqtrid	$⊢ x \cap ⋃ b = \emptyset \to (⋃ b \cup x) ∖ ⋃ b = x$
100	84 99	syl	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cup x) ∖ ⋃ b = x$
101	100	ineq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap ((⋃ b \cup x) ∖ ⋃ b) = E \cap x$
102	92 101	eqtr3id	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (E \cap (⋃ b \cup x)) ∖ ⋃ b = E \cap x$
103	102	fveq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap x)$
104	91 103	oveq12d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) \cap ⋃ b) +_{𝑒} M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap ⋃ b) +_{𝑒} M (E \cap x)$
105	1	adantr	$⊢ (φ \land b \subseteq A) \to O \in V$
106	2	adantr	$⊢ (φ \land b \subseteq A) \to M : 𝒫 O ⟶ [0, +∞]$
107	3	adantr	$⊢ (φ \land b \subseteq A) \to M (\emptyset) = 0$
108	4	3adant1r	$⊢ ((φ \land b \subseteq A) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
109		ssfi	$⊢ (A \in Fin \land b \subseteq A) \to b \in Fin$
110	5 109	sylan	$⊢ (φ \land b \subseteq A) \to b \in Fin$
111	6	adantr	$⊢ (φ \land b \subseteq A) \to A \subseteq toCaraSiga (M)$
112	81 111	sstrd	$⊢ (φ \land b \subseteq A) \to b \subseteq toCaraSiga (M)$
113	105 106 107 108 110 112	fiunelcarsg	$⊢ (φ \land b \subseteq A) \to ⋃ b \in toCaraSiga (M)$
114	1 2	elcarsg	$⊢ φ \to (⋃ b \in toCaraSiga (M) \leftrightarrow (⋃ b \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)))$
115	114	adantr	$⊢ (φ \land b \subseteq A) \to (⋃ b \in toCaraSiga (M) \leftrightarrow (⋃ b \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)))$
116	113 115	mpbid	$⊢ (φ \land b \subseteq A) \to (⋃ b \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e))$
117	116	simprd	$⊢ (φ \land b \subseteq A) \to \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)$
118	117	adantrr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)$
119	43	elpwincl1	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap (⋃ b \cup x) \in 𝒫 O$
120		simpr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to e = E \cap (⋃ b \cup x)$
121	120	ineq1d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to e \cap ⋃ b = (E \cap (⋃ b \cup x)) \cap ⋃ b$
122	121	fveq2d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to M (e \cap ⋃ b) = M ((E \cap (⋃ b \cup x)) \cap ⋃ b)$
123	120	difeq1d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to e ∖ ⋃ b = (E \cap (⋃ b \cup x)) ∖ ⋃ b$
124	123	fveq2d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to M (e ∖ ⋃ b) = M ((E \cap (⋃ b \cup x)) ∖ ⋃ b)$
125	122 124	oveq12d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M ((E \cap (⋃ b \cup x)) \cap ⋃ b) +_{𝑒} M ((E \cap (⋃ b \cup x)) ∖ ⋃ b)$
126	120	fveq2d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to M (e) = M (E \cap (⋃ b \cup x))$
127	125 126	eqeq12d	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to (M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e) \leftrightarrow M ((E \cap (⋃ b \cup x)) \cap ⋃ b) +_{𝑒} M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap (⋃ b \cup x)))$
128	119 127	rspcdv	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (\forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e) \to M ((E \cap (⋃ b \cup x)) \cap ⋃ b) +_{𝑒} M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap (⋃ b \cup x)))$
129	118 128	mpd	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) \cap ⋃ b) +_{𝑒} M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap (⋃ b \cup x))$
130	104 129	eqtr3d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M (E \cap ⋃ b) +_{𝑒} M (E \cap x) = M (E \cap (⋃ b \cup x))$
131	130	adantr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{*}} M (E \cap y)) \to M (E \cap ⋃ b) +_{𝑒} M (E \cap x) = M (E \cap (⋃ b \cup x))$
132	74 131	eqtr4id	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{*}} M (E \cap y)) \to M (E \cap ⋃ (b \cup \{x\})) = M (E \cap ⋃ b) +_{𝑒} M (E \cap x)$
133	48 68 132	3eqtr4rd	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y)) \to M (E \cap ⋃ (b \cup \{x\})) = \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y)$
134	133	ex	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (M (E \cap ⋃ b) = \underset{y \in b}{\sum^{}} M (E \cap y) \to M (E \cap ⋃ (b \cup \{x\})) = \underset{y \in b \cup \{x\}}{\sum^{}} M (E \cap y))$
135	13 18 23 28 35 134 5	findcard2d	$⊢ φ \to M (E \cap ⋃ A) = \underset{y \in A}{\sum^{*}} M (E \cap y)$

Metamath Proof Explorer

Theorem carsgclctunlem1

Proof