ltexprlem4

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 6-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	ltexprlem4	$⊢ B \in 𝑷 \to (x \in C \to \exists z (z \in C \land x <_{𝑸} z))$

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	$⊢ C = \{x \| \exists y (\neg y \in A \land y +_{𝑸} x \in B)\}$
2		prnmax	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to \exists w \in B (y +_{𝑸} x) <_{𝑸} w$
3		df-rex	$⊢ \exists w \in B (y +_{𝑸} x) <_{𝑸} w \leftrightarrow \exists w (w \in B \land (y +_{𝑸} x) <_{𝑸} w)$
4	2 3	sylib	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to \exists w (w \in B \land (y +_{𝑸} x) <_{𝑸} w)$
5		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
6	5	brel	$⊢ (y +_{𝑸} x) <_{𝑸} w \to (y +_{𝑸} x \in 𝑸 \land w \in 𝑸)$
7	6	simpld	$⊢ (y +_{𝑸} x) <_{𝑸} w \to y +_{𝑸} x \in 𝑸$
8		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
9	8	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
10		0nnq	$⊢ \neg \emptyset \in 𝑸$
11	9 10	ndmovrcl	$⊢ y +_{𝑸} x \in 𝑸 \to (y \in 𝑸 \land x \in 𝑸)$
12	7 11	syl	$⊢ (y +_{𝑸} x) <_{𝑸} w \to (y \in 𝑸 \land x \in 𝑸)$
13		ltaddnq	$⊢ (y \in 𝑸 \land x \in 𝑸) \to y <_{𝑸} (y +_{𝑸} x)$
14		ltsonq	$⊢ <_{𝑸} Or 𝑸$
15	14 5	sotri	$⊢ (y <_{𝑸} (y +_{𝑸} x) \land (y +_{𝑸} x) <_{𝑸} w) \to y <_{𝑸} w$
16	13 15	sylan	$⊢ ((y \in 𝑸 \land x \in 𝑸) \land (y +_{𝑸} x) <_{𝑸} w) \to y <_{𝑸} w$
17	12 16	mpancom	$⊢ (y +_{𝑸} x) <_{𝑸} w \to y <_{𝑸} w$
18	5	brel	$⊢ y <_{𝑸} w \to (y \in 𝑸 \land w \in 𝑸)$
19	18	simprd	$⊢ y <_{𝑸} w \to w \in 𝑸$
20		ltexnq	$⊢ w \in 𝑸 \to (y <_{𝑸} w \leftrightarrow \exists z y +_{𝑸} z = w)$
21	20	biimpd	$⊢ w \in 𝑸 \to (y <_{𝑸} w \to \exists z y +_{𝑸} z = w)$
22	19 21	mpcom	$⊢ y <_{𝑸} w \to \exists z y +_{𝑸} z = w$
23	17 22	syl	$⊢ (y +_{𝑸} x) <_{𝑸} w \to \exists z y +_{𝑸} z = w$
24		eqcom	$⊢ w = y +_{𝑸} z \leftrightarrow y +_{𝑸} z = w$
25	24	exbii	$⊢ \exists z w = y +_{𝑸} z \leftrightarrow \exists z y +_{𝑸} z = w$
26	23 25	sylibr	$⊢ (y +_{𝑸} x) <_{𝑸} w \to \exists z w = y +_{𝑸} z$
27	26	ancri	$⊢ (y +_{𝑸} x) <_{𝑸} w \to (\exists z w = y +_{𝑸} z \land (y +_{𝑸} x) <_{𝑸} w)$
28	27	anim2i	$⊢ (w \in B \land (y +_{𝑸} x) <_{𝑸} w) \to (w \in B \land (\exists z w = y +_{𝑸} z \land (y +_{𝑸} x) <_{𝑸} w))$
29		an12	$⊢ (\exists z w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \leftrightarrow (w \in B \land (\exists z w = y +_{𝑸} z \land (y +_{𝑸} x) <_{𝑸} w))$
30	28 29	sylibr	$⊢ (w \in B \land (y +_{𝑸} x) <_{𝑸} w) \to (\exists z w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
31		19.41v	$⊢ \exists z (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \leftrightarrow (\exists z w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
32	30 31	sylibr	$⊢ (w \in B \land (y +_{𝑸} x) <_{𝑸} w) \to \exists z (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
33	32	eximi	$⊢ \exists w (w \in B \land (y +_{𝑸} x) <_{𝑸} w) \to \exists w \exists z (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
34		excom	$⊢ \exists z \exists w (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \leftrightarrow \exists w \exists z (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
35	33 34	sylibr	$⊢ \exists w (w \in B \land (y +_{𝑸} x) <_{𝑸} w) \to \exists z \exists w (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w))$
36		ovex	$⊢ y +_{𝑸} z \in V$
37		eleq1	$⊢ w = y +_{𝑸} z \to (w \in B \leftrightarrow y +_{𝑸} z \in B)$
38		breq2	$⊢ w = y +_{𝑸} z \to ((y +_{𝑸} x) <_{𝑸} w \leftrightarrow (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z))$
39	37 38	anbi12d	$⊢ w = y +_{𝑸} z \to ((w \in B \land (y +_{𝑸} x) <_{𝑸} w) \leftrightarrow (y +_{𝑸} z \in B \land (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z)))$
40	36 39	ceqsexv	$⊢ \exists w (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \leftrightarrow (y +_{𝑸} z \in B \land (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z))$
41		ltanq	$⊢ y \in 𝑸 \to (x <_{𝑸} z \leftrightarrow (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z))$
42	9 5 10 41	ndmovordi	$⊢ (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z) \to x <_{𝑸} z$
43	42	anim2i	$⊢ (y +_{𝑸} z \in B \land (y +_{𝑸} x) <_{𝑸} (y +_{𝑸} z)) \to (y +_{𝑸} z \in B \land x <_{𝑸} z)$
44	40 43	sylbi	$⊢ \exists w (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \to (y +_{𝑸} z \in B \land x <_{𝑸} z)$
45	44	eximi	$⊢ \exists z \exists w (w = y +_{𝑸} z \land (w \in B \land (y +_{𝑸} x) <_{𝑸} w)) \to \exists z (y +_{𝑸} z \in B \land x <_{𝑸} z)$
46	4 35 45	3syl	$⊢ (B \in 𝑷 \land y +_{𝑸} x \in B) \to \exists z (y +_{𝑸} z \in B \land x <_{𝑸} z)$
47	46	anim2i	$⊢ (\neg y \in A \land (B \in 𝑷 \land y +_{𝑸} x \in B)) \to (\neg y \in A \land \exists z (y +_{𝑸} z \in B \land x <_{𝑸} z))$
48	47	an12s	$⊢ (B \in 𝑷 \land (\neg y \in A \land y +_{𝑸} x \in B)) \to (\neg y \in A \land \exists z (y +_{𝑸} z \in B \land x <_{𝑸} z))$
49		19.42v	$⊢ \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z)) \leftrightarrow (\neg y \in A \land \exists z (y +_{𝑸} z \in B \land x <_{𝑸} z))$
50	48 49	sylibr	$⊢ (B \in 𝑷 \land (\neg y \in A \land y +_{𝑸} x \in B)) \to \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
51	50	ex	$⊢ B \in 𝑷 \to ((\neg y \in A \land y +_{𝑸} x \in B) \to \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z)))$
52	51	eximdv	$⊢ B \in 𝑷 \to (\exists y (\neg y \in A \land y +_{𝑸} x \in B) \to \exists y \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z)))$
53	1	eqabri	$⊢ x \in C \leftrightarrow \exists y (\neg y \in A \land y +_{𝑸} x \in B)$
54		vex	$⊢ z \in V$
55		oveq2	$⊢ x = z \to y +_{𝑸} x = y +_{𝑸} z$
56	55	eleq1d	$⊢ x = z \to (y +_{𝑸} x \in B \leftrightarrow y +_{𝑸} z \in B)$
57	56	anbi2d	$⊢ x = z \to ((\neg y \in A \land y +_{𝑸} x \in B) \leftrightarrow (\neg y \in A \land y +_{𝑸} z \in B))$
58	57	exbidv	$⊢ x = z \to (\exists y (\neg y \in A \land y +_{𝑸} x \in B) \leftrightarrow \exists y (\neg y \in A \land y +_{𝑸} z \in B))$
59	54 58 1	elab2	$⊢ z \in C \leftrightarrow \exists y (\neg y \in A \land y +_{𝑸} z \in B)$
60	59	anbi1i	$⊢ (z \in C \land x <_{𝑸} z) \leftrightarrow (\exists y (\neg y \in A \land y +_{𝑸} z \in B) \land x <_{𝑸} z)$
61		19.41v	$⊢ \exists y ((\neg y \in A \land y +_{𝑸} z \in B) \land x <_{𝑸} z) \leftrightarrow (\exists y (\neg y \in A \land y +_{𝑸} z \in B) \land x <_{𝑸} z)$
62		anass	$⊢ ((\neg y \in A \land y +_{𝑸} z \in B) \land x <_{𝑸} z) \leftrightarrow (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
63	62	exbii	$⊢ \exists y ((\neg y \in A \land y +_{𝑸} z \in B) \land x <_{𝑸} z) \leftrightarrow \exists y (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
64	60 61 63	3bitr2i	$⊢ (z \in C \land x <_{𝑸} z) \leftrightarrow \exists y (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
65	64	exbii	$⊢ \exists z (z \in C \land x <_{𝑸} z) \leftrightarrow \exists z \exists y (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
66		excom	$⊢ \exists y \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z)) \leftrightarrow \exists z \exists y (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
67	65 66	bitr4i	$⊢ \exists z (z \in C \land x <_{𝑸} z) \leftrightarrow \exists y \exists z (\neg y \in A \land (y +_{𝑸} z \in B \land x <_{𝑸} z))$
68	52 53 67	3imtr4g	$⊢ B \in 𝑷 \to (x \in C \to \exists z (z \in C \land x <_{𝑸} z))$

Metamath Proof Explorer

Theorem ltexprlem4

Proof