ltexprlem6

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ltexprlem.1	$⊢ C = \{x \| \exists y (\neg y \in A \land y +_{𝑸} x \in B)\}$
	Assertion	ltexprlem6	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land A \subset B) \to A +_{𝑷} C \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	$⊢ C = \{x \| \exists y (\neg y \in A \land y +_{𝑸} x \in B)\}$
2	1	ltexprlem5	$⊢ (B \in 𝑷 \land A \subset B) \to C \in 𝑷$
3		df-plp	$⊢ +_{𝑷} = (z \in 𝑷, y \in 𝑷 ⟼ \{f \| \exists g \in z \exists h \in y f = g +_{𝑸} h\})$
4		addclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g +_{𝑸} h \in 𝑸$
5	3 4	genpelv	$⊢ (A \in 𝑷 \land C \in 𝑷) \to (z \in (A +_{𝑷} C) \leftrightarrow \exists w \in A \exists x \in C z = w +_{𝑸} x)$
6	2 5	sylan2	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land A \subset B)) \to (z \in (A +_{𝑷} C) \leftrightarrow \exists w \in A \exists x \in C z = w +_{𝑸} x)$
7	1	eqabri	$⊢ x \in C \leftrightarrow \exists y (\neg y \in A \land y +_{𝑸} x \in B)$
8		elprnq	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to y +_{𝑸} x \in 𝑸$
9		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
10	9	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
11		0nnq	$⊢ \neg \emptyset \in 𝑸$
12	10 11	ndmovrcl	$⊢ y +_{𝑸} x \in 𝑸 \to (y \in 𝑸 \land x \in 𝑸)$
13	12	simpld	$⊢ y +_{𝑸} x \in 𝑸 \to y \in 𝑸$
14	8 13	syl	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to y \in 𝑸$
15		prub	$⊢ ((A \in 𝑷 \land w \in A) \land y \in 𝑸) \to (\neg y \in A \to w <_{𝑸} y)$
16	14 15	sylan2	$⊢ ((A \in 𝑷 \land w \in A) \land (B \in 𝑷 \land y +_{𝑸} x \in B)) \to (\neg y \in A \to w <_{𝑸} y)$
17	12	simprd	$⊢ y +_{𝑸} x \in 𝑸 \to x \in 𝑸$
18		vex	$⊢ w \in V$
19		vex	$⊢ y \in V$
20		ltanq	$⊢ u \in 𝑸 \to (z <_{𝑸} v \leftrightarrow (u +_{𝑸} z) <_{𝑸} (u +_{𝑸} v))$
21		vex	$⊢ x \in V$
22		addcomnq	$⊢ z +_{𝑸} v = v +_{𝑸} z$
23	18 19 20 21 22	caovord2	$⊢ x \in 𝑸 \to (w <_{𝑸} y \leftrightarrow (w +_{𝑸} x) <_{𝑸} (y +_{𝑸} x))$
24	8 17 23	3syl	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to (w <_{𝑸} y \leftrightarrow (w +_{𝑸} x) <_{𝑸} (y +_{𝑸} x))$
25		prcdnq	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to ((w +_{𝑸} x) <_{𝑸} (y +_{𝑸} x) \to w +_{𝑸} x \in B)$
26	24 25	sylbid	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to (w <_{𝑸} y \to w +_{𝑸} x \in B)$
27	26	adantl	$⊢ ((A \in 𝑷 \land w \in A) \land (B \in 𝑷 \land y +_{𝑸} x \in B)) \to (w <_{𝑸} y \to w +_{𝑸} x \in B)$
28	16 27	syld	$⊢ ((A \in 𝑷 \land w \in A) \land (B \in 𝑷 \land y +_{𝑸} x \in B)) \to (\neg y \in A \to w +_{𝑸} x \in B)$
29	28	exp32	$⊢ (A \in 𝑷 \land w \in A) \to (B \in 𝑷 \to (y +_{𝑸} x \in B \to (\neg y \in A \to w +_{𝑸} x \in B)))$
30	29	com34	$⊢ (A \in 𝑷 \land w \in A) \to (B \in 𝑷 \to (\neg y \in A \to (y +_{𝑸} x \in B \to w +_{𝑸} x \in B)))$
31	30	imp4b	$⊢ ((A \in 𝑷 \land w \in A) \land B \in 𝑷) \to ((\neg y \in A \land y +_{𝑸} x \in B) \to w +_{𝑸} x \in B)$
32	31	exlimdv	$⊢ ((A \in 𝑷 \land w \in A) \land B \in 𝑷) \to (\exists y (\neg y \in A \land y +_{𝑸} x \in B) \to w +_{𝑸} x \in B)$
33	7 32	biimtrid	$⊢ ((A \in 𝑷 \land w \in A) \land B \in 𝑷) \to (x \in C \to w +_{𝑸} x \in B)$
34	33	exp31	$⊢ A \in 𝑷 \to (w \in A \to (B \in 𝑷 \to (x \in C \to w +_{𝑸} x \in B)))$
35	34	com23	$⊢ A \in 𝑷 \to (B \in 𝑷 \to (w \in A \to (x \in C \to w +_{𝑸} x \in B)))$
36	35	imp43	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (w \in A \land x \in C)) \to w +_{𝑸} x \in B$
37		eleq1	$⊢ z = w +_{𝑸} x \to (z \in B \leftrightarrow w +_{𝑸} x \in B)$
38	37	biimparc	$⊢ (w +_{𝑸} x \in B \land z = w +_{𝑸} x) \to z \in B$
39	36 38	sylan	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (w \in A \land x \in C)) \land z = w +_{𝑸} x) \to z \in B$
40	39	exp31	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((w \in A \land x \in C) \to (z = w +_{𝑸} x \to z \in B))$
41	40	rexlimdvv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists w \in A \exists x \in C z = w +_{𝑸} x \to z \in B)$
42	41	adantrr	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land A \subset B)) \to (\exists w \in A \exists x \in C z = w +_{𝑸} x \to z \in B)$
43	6 42	sylbid	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land A \subset B)) \to (z \in (A +_{𝑷} C) \to z \in B)$
44	43	ssrdv	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land A \subset B)) \to A +_{𝑷} C \subseteq B$
45	44	anassrs	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land A \subset B) \to A +_{𝑷} C \subseteq B$

Metamath Proof Explorer

Theorem ltexprlem6

Proof