Theorem 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=\left\{x|\exists y\left(\neg y\in A\wedge y{+}_{𝑸}x\in B\right)\right\}$$
Assertion	ltexprlem2	$$⊢B\in 𝑷\to C\subset 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	$$⊢C=\left\{x|\exists y\left(\neg y\in A\wedge y{+}_{𝑸}x\in B\right)\right\}$$
2	1	abeq2i	$$⊢x\in C\leftrightarrow \exists y\left(\neg y\in A\wedge y{+}_{𝑸}x\in B\right)$$
3		elprnq	$$⊢\left(B\in 𝑷\wedge y{+}_{𝑸}x\in B\right)\to y{+}_{𝑸}x\in 𝑸$$
4		addnqf	$$⊢{+}_{𝑸}:𝑸\times 𝑸⟶𝑸$$
5	4	fdmi	$$⊢\mathrm{dom}{+}_{𝑸}=𝑸\times 𝑸$$
6		0nnq	$$⊢\neg \varnothing \in 𝑸$$
7	5 6	ndmovrcl	$$⊢y{+}_{𝑸}x\in 𝑸\to \left(y\in 𝑸\wedge x\in 𝑸\right)$$
8	3 7	syl	$$⊢\left(B\in 𝑷\wedge y{+}_{𝑸}x\in B\right)\to \left(y\in 𝑸\wedge x\in 𝑸\right)$$
9		ltaddnq	$$⊢\left(x\in 𝑸\wedge y\in 𝑸\right)\to x{<}_{𝑸}\left(x{+}_{𝑸}y\right)$$
10	9	ancoms	$$⊢\left(y\in 𝑸\wedge x\in 𝑸\right)\to x{<}_{𝑸}\left(x{+}_{𝑸}y\right)$$
11		addcomnq	$$⊢x{+}_{𝑸}y=y{+}_{𝑸}x$$
12	10 11	breqtrdi	$$⊢\left(y\in 𝑸\wedge x\in 𝑸\right)\to x{<}_{𝑸}\left(y{+}_{𝑸}x\right)$$
13		prcdnq	$$⊢\left(B\in 𝑷\wedge y{+}_{𝑸}x\in B\right)\to \left(x{<}_{𝑸}\left(y{+}_{𝑸}x\right)\to x\in B\right)$$
14	12 13	syl5	$$⊢\left(B\in 𝑷\wedge y{+}_{𝑸}x\in B\right)\to \left(\left(y\in 𝑸\wedge x\in 𝑸\right)\to x\in B\right)$$
15	8 14	mpd	$$⊢\left(B\in 𝑷\wedge y{+}_{𝑸}x\in B\right)\to x\in B$$
16	15	ex	$$⊢B\in 𝑷\to \left(y{+}_{𝑸}x\in B\to x\in B\right)$$
17	16	adantld	$$⊢B\in 𝑷\to \left(\left(\neg y\in A\wedge y{+}_{𝑸}x\in B\right)\to x\in B\right)$$
18	17	exlimdv	$$⊢B\in 𝑷\to \left(\exists y\left(\neg y\in A\wedge y{+}_{𝑸}x\in B\right)\to x\in B\right)$$
19	2 18	syl5bi	$$⊢B\in 𝑷\to \left(x\in C\to x\in B\right)$$
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 𝑸$$