ltexprlem2

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 3-Apr-1996) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	$⊢ C = \{x \| \exists y (\neg y \in A \land y +_{𝑸} x \in B)\}$
2	1	eqabri	$⊢ x \in C \leftrightarrow \exists y (\neg y \in A \land y +_{𝑸} x \in B)$
3		elprnq	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to y +_{𝑸} x \in 𝑸$
4		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
5	4	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
6		0nnq	$⊢ \neg \emptyset \in 𝑸$
7	5 6	ndmovrcl	$⊢ y +_{𝑸} x \in 𝑸 \to (y \in 𝑸 \land x \in 𝑸)$
8	3 7	syl	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to (y \in 𝑸 \land x \in 𝑸)$
9		ltaddnq	$⊢ (x \in 𝑸 \land y \in 𝑸) \to x <_{𝑸} (x +_{𝑸} y)$
10	9	ancoms	$⊢ (y \in 𝑸 \land x \in 𝑸) \to x <_{𝑸} (x +_{𝑸} y)$
11		addcomnq	$⊢ x +_{𝑸} y = y +_{𝑸} x$
12	10 11	breqtrdi	$⊢ (y \in 𝑸 \land x \in 𝑸) \to x <_{𝑸} (y +_{𝑸} x)$
13		prcdnq	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to (x <_{𝑸} (y +_{𝑸} x) \to x \in B)$
14	12 13	syl5	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to ((y \in 𝑸 \land x \in 𝑸) \to x \in B)$
15	8 14	mpd	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to x \in B$
16	15	ex	$⊢ B \in 𝑷 \to (y +_{𝑸} x \in B \to x \in B)$
17	16	adantld	$⊢ B \in 𝑷 \to ((\neg y \in A \land y +_{𝑸} x \in B) \to x \in B)$
18	17	exlimdv	$⊢ B \in 𝑷 \to (\exists y (\neg y \in A \land y +_{𝑸} x \in B) \to x \in B)$
19	2 18	biimtrid	$⊢ B \in 𝑷 \to (x \in C \to x \in B)$
20	19	ssrdv	$⊢ B \in 𝑷 \to C \subseteq B$
21		prpssnq	$⊢ B \in 𝑷 \to B \subset 𝑸$
22	20 21	sspsstrd	$⊢ B \in 𝑷 \to C \subset 𝑸$

Metamath Proof Explorer

Theorem ltexprlem2

Proof