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	ffvelrnd	$⊢ (φ \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		snex	$⊢ \{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	ffvelrnd	$⊢ ((φ \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	ffvelrnd	$⊢ ((φ \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		vex	$⊢ x \in V$
71	70	unisn	$⊢ ⋃ \{x\} = x$
72	71	uneq2i	$⊢ ⋃ b \cup ⋃ \{x\} = ⋃ b \cup x$
73	69 72	eqtri	$⊢ ⋃ (b \cup \{x\}) = ⋃ b \cup x$
74	73	ineq2i	$⊢ E \cap ⋃ (b \cup \{x\}) = E \cap (⋃ b \cup x)$
75	74	fveq2i	$⊢ M (E \cap ⋃ (b \cup \{x\})) = M (E \cap (⋃ b \cup x))$
76		inass	$⊢ (E \cap (⋃ b \cup x)) \cap ⋃ b = E \cap ((⋃ b \cup x) \cap ⋃ b)$
77		indir	$⊢ (⋃ b \cup x) \cap ⋃ b = (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b)$
78		inidm	$⊢ ⋃ b \cap ⋃ b = ⋃ b$
79	78	a1i	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to ⋃ b \cap ⋃ b = ⋃ b$
80		incom	$⊢ ⋃ b \cap x = x \cap ⋃ b$
81	7	adantr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \underset{y \in A}{Disj} y$
82		simpr	$⊢ (φ \land b \subseteq A) \to b \subseteq A$
83	82	adantrr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to b \subseteq A$
84	81 83 41	disjuniel	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to ⋃ b \cap x = \emptyset$
85	80 84	eqtr3id	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to x \cap ⋃ b = \emptyset$
86	79 85	uneq12d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b) = ⋃ b \cup \emptyset$
87		un0	$⊢ ⋃ b \cup \emptyset = ⋃ b$
88	86 87	eqtrdi	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cap ⋃ b) \cup (x \cap ⋃ b) = ⋃ b$
89	77 88	syl5eq	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cup x) \cap ⋃ b = ⋃ b$
90	89	ineq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap ((⋃ b \cup x) \cap ⋃ b) = E \cap ⋃ b$
91	76 90	syl5eq	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (E \cap (⋃ b \cup x)) \cap ⋃ b = E \cap ⋃ b$
92	91	fveq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) \cap ⋃ b) = M (E \cap ⋃ b)$
93		indif2	$⊢ E \cap ((⋃ b \cup x) ∖ ⋃ b) = (E \cap (⋃ b \cup x)) ∖ ⋃ b$
94		uncom	$⊢ ⋃ b \cup x = x \cup ⋃ b$
95	94	difeq1i	$⊢ (⋃ b \cup x) ∖ ⋃ b = (x \cup ⋃ b) ∖ ⋃ b$
96		difun2	$⊢ (x \cup ⋃ b) ∖ ⋃ b = x ∖ ⋃ b$
97		disj3	$⊢ x \cap ⋃ b = \emptyset \leftrightarrow x = x ∖ ⋃ b$
98	97	biimpi	$⊢ x \cap ⋃ b = \emptyset \to x = x ∖ ⋃ b$
99	96 98	eqtr4id	$⊢ x \cap ⋃ b = \emptyset \to (x \cup ⋃ b) ∖ ⋃ b = x$
100	95 99	syl5eq	$⊢ x \cap ⋃ b = \emptyset \to (⋃ b \cup x) ∖ ⋃ b = x$
101	85 100	syl	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \cup x) ∖ ⋃ b = x$
102	101	ineq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap ((⋃ b \cup x) ∖ ⋃ b) = E \cap x$
103	93 102	eqtr3id	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (E \cap (⋃ b \cup x)) ∖ ⋃ b = E \cap x$
104	103	fveq2d	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to M ((E \cap (⋃ b \cup x)) ∖ ⋃ b) = M (E \cap x)$
105	92 104	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)$
106	1	adantr	$⊢ (φ \land b \subseteq A) \to O \in V$
107	2	adantr	$⊢ (φ \land b \subseteq A) \to M : 𝒫 O ⟶ [0, +∞]$
108	3	adantr	$⊢ (φ \land b \subseteq A) \to M (\emptyset) = 0$
109	4	3adant1r	$⊢ ((φ \land b \subseteq A) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
110		ssfi	$⊢ (A \in Fin \land b \subseteq A) \to b \in Fin$
111	5 110	sylan	$⊢ (φ \land b \subseteq A) \to b \in Fin$
112	6	adantr	$⊢ (φ \land b \subseteq A) \to A \subseteq toCaraSiga (M)$
113	82 112	sstrd	$⊢ (φ \land b \subseteq A) \to b \subseteq toCaraSiga (M)$
114	106 107 108 109 111 113	fiunelcarsg	$⊢ (φ \land b \subseteq A) \to ⋃ b \in toCaraSiga (M)$
115	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)))$
116	115	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)))$
117	114 116	mpbid	$⊢ (φ \land b \subseteq A) \to (⋃ b \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e))$
118	117	simprd	$⊢ (φ \land b \subseteq A) \to \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)$
119	118	adantrr	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to \forall e \in 𝒫 O M (e \cap ⋃ b) +_{𝑒} M (e ∖ ⋃ b) = M (e)$
120	43	elpwincl1	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to E \cap (⋃ b \cup x) \in 𝒫 O$
121		simpr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land e = E \cap (⋃ b \cup x)) \to e = E \cap (⋃ b \cup x)$
122	121	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$
123	122	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)$
124	121	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$
125	124	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)$
126	123 125	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)$
127	121	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))$
128	126 127	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)))$
129	120 128	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)))$
130	119 129	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))$
131	105 130	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))$
132	131	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))$
133	75 132	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)$
134	48 68 133	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)$
135	134	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))$
136	13 18 23 28 35 135 5	findcard2d	$⊢ φ \to M (E \cap ⋃ A) = \underset{y \in A}{\sum^{*}} M (E \cap y)$

Metamath Proof Explorer

Theorem carsgclctunlem1

Proof