Theorem ltexprlemloc 6580

Description: Our constructed difference is located. Lemma for ltexpri 6586. (Contributed by Jim Kingdon, 17-Dec-2019.)

Hypothesis

Ref	Expression
ltexprlem.1	⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩

Assertion

Ref	Expression
ltexprlemloc	⊢ (A<P B → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))

Distinct variable groups:   x,y,𝑞,𝑟,A   x,B,y,𝑞,𝑟   x,𝐶,y,𝑞,𝑟

Proof of Theorem ltexprlemloc

Dummy variables z w f g ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltexnqi 6392	. . . . . 6 ⊢ (𝑞 <Q 𝑟 → ∃w ∈ Q (𝑞 +Q w) = 𝑟)
2	1	adantl 262	. . . . 5 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → ∃w ∈ Q (𝑞 +Q w) = 𝑟)
3		ltrelpr 6487	. . . . . . . . . 10 ⊢ <P ⊆ (P × P)
4	3	brel 4335	. . . . . . . . 9 ⊢ (A<P B → (A ∈ P ∧ B ∈ P))
5	4	simpld 105	. . . . . . . 8 ⊢ (A<P B → A ∈ P)
6		prop 6457	. . . . . . . . 9 ⊢ (A ∈ P → ⟨(1st ‘A), (2nd ‘A)⟩ ∈ P)
7		prarloc 6485	. . . . . . . . 9 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ w ∈ Q) → ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w))
8	6, 7	sylan 267	. . . . . . . 8 ⊢ ((A ∈ P ∧ w ∈ Q) → ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w))
9	5, 8	sylan 267	. . . . . . 7 ⊢ ((A<P B ∧ w ∈ Q) → ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w))
10	9	ad2ant2r 478	. . . . . 6 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w))
11	4	simprd 107	. . . . . . . . . . . . . 14 ⊢ (A<P B → B ∈ P)
12	11	ad2antrr 457	. . . . . . . . . . . . 13 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → B ∈ P)
13	12	ad2antrr 457	. . . . . . . . . . . 12 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → B ∈ P)
14		ltanqg 6384	. . . . . . . . . . . . . . . 16 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g)))
15	14	adantl 262	. . . . . . . . . . . . . . 15 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → (f <Q g ↔ (ℎ +Q f) <Q (ℎ +Q g)))
16		elprnqu 6464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ y ∈ (2nd ‘A)) → y ∈ Q)
17	6, 16	sylan 267	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ P ∧ y ∈ (2nd ‘A)) → y ∈ Q)
18	5, 17	sylan 267	. . . . . . . . . . . . . . . . 17 ⊢ ((A<P B ∧ y ∈ (2nd ‘A)) → y ∈ Q)
19	18	adantlr 446	. . . . . . . . . . . . . . . 16 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ y ∈ (2nd ‘A)) → y ∈ Q)
20	19	ad2ant2rl 480	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → y ∈ Q)
21		elprnql 6463	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ z ∈ (1st ‘A)) → z ∈ Q)
22	6, 21	sylan 267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ P ∧ z ∈ (1st ‘A)) → z ∈ Q)
23	5, 22	sylan 267	. . . . . . . . . . . . . . . . . 18 ⊢ ((A<P B ∧ z ∈ (1st ‘A)) → z ∈ Q)
24	23	adantlr 446	. . . . . . . . . . . . . . . . 17 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ z ∈ (1st ‘A)) → z ∈ Q)
25	24	ad2ant2r 478	. . . . . . . . . . . . . . . 16 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → z ∈ Q)
26		simplrl 487	. . . . . . . . . . . . . . . 16 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → w ∈ Q)
27		addclnq 6359	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ Q ∧ w ∈ Q) → (z +Q w) ∈ Q)
28	25, 26, 27	syl2anc 391	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (z +Q w) ∈ Q)
29		ltrelnq 6349	. . . . . . . . . . . . . . . . . . 19 ⊢ <Q ⊆ (Q × Q)
30	29	brel 4335	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 <Q 𝑟 → (𝑞 ∈ Q ∧ 𝑟 ∈ Q))
31	30	simpld 105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 <Q 𝑟 → 𝑞 ∈ Q)
32	31	adantl 262	. . . . . . . . . . . . . . . 16 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → 𝑞 ∈ Q)
33	32	ad2antrr 457	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → 𝑞 ∈ Q)
34		addcomnqg 6365	. . . . . . . . . . . . . . . 16 ⊢ ((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g +Q f))
35	34	adantl 262	. . . . . . . . . . . . . . 15 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ (f ∈ Q ∧ g ∈ Q)) → (f +Q g) = (g +Q f))
36	15, 20, 28, 33, 35	caovord2d 5612	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (y <Q (z +Q w) ↔ (y +Q 𝑞) <Q ((z +Q w) +Q 𝑞)))
37		addassnqg 6366	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ Q ∧ w ∈ Q ∧ 𝑞 ∈ Q) → ((z +Q w) +Q 𝑞) = (z +Q (w +Q 𝑞)))
38	25, 26, 33, 37	syl3anc 1134	. . . . . . . . . . . . . . . 16 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → ((z +Q w) +Q 𝑞) = (z +Q (w +Q 𝑞)))
39		addcomnqg 6365	. . . . . . . . . . . . . . . . . 18 ⊢ ((w ∈ Q ∧ 𝑞 ∈ Q) → (w +Q 𝑞) = (𝑞 +Q w))
40	26, 33, 39	syl2anc 391	. . . . . . . . . . . . . . . . 17 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (w +Q 𝑞) = (𝑞 +Q w))
41	40	oveq2d 5471	. . . . . . . . . . . . . . . 16 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (z +Q (w +Q 𝑞)) = (z +Q (𝑞 +Q w)))
42		simplrr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (𝑞 +Q w) = 𝑟)
43	42	oveq2d 5471	. . . . . . . . . . . . . . . 16 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (z +Q (𝑞 +Q w)) = (z +Q 𝑟))
44	38, 41, 43	3eqtrd 2073	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → ((z +Q w) +Q 𝑞) = (z +Q 𝑟))
45	44	breq2d 3767	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → ((y +Q 𝑞) <Q ((z +Q w) +Q 𝑞) ↔ (y +Q 𝑞) <Q (z +Q 𝑟)))
46	36, 45	bitrd 177	. . . . . . . . . . . . 13 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (y <Q (z +Q w) ↔ (y +Q 𝑞) <Q (z +Q 𝑟)))
47	46	biimpa 280	. . . . . . . . . . . 12 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → (y +Q 𝑞) <Q (z +Q 𝑟))
48		prop 6457	. . . . . . . . . . . . 13 ⊢ (B ∈ P → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
49		prloc 6473	. . . . . . . . . . . . 13 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ (y +Q 𝑞) <Q (z +Q 𝑟)) → ((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)))
50	48, 49	sylan 267	. . . . . . . . . . . 12 ⊢ ((B ∈ P ∧ (y +Q 𝑞) <Q (z +Q 𝑟)) → ((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)))
51	13, 47, 50	syl2anc 391	. . . . . . . . . . 11 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) ∧ y <Q (z +Q w)) → ((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)))
52	51	ex 108	. . . . . . . . . 10 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ (z ∈ (1st ‘A) ∧ y ∈ (2nd ‘A))) → (y <Q (z +Q w) → ((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
53	52	anassrs 380	. . . . . . . . 9 ⊢ (((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ z ∈ (1st ‘A)) ∧ y ∈ (2nd ‘A)) → (y <Q (z +Q w) → ((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
54	53	reximdva 2415	. . . . . . . 8 ⊢ ((((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) ∧ z ∈ (1st ‘A)) → (∃y ∈ (2nd ‘A)y <Q (z +Q w) → ∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
55	54	reximdva 2415	. . . . . . 7 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w) → ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
56		prml 6459	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘A), (2nd ‘A)⟩ ∈ P → ∃z ∈ Q z ∈ (1st ‘A))
57		rexex 2362	. . . . . . . . . . . 12 ⊢ (∃z ∈ Q z ∈ (1st ‘A) → ∃z z ∈ (1st ‘A))
58	6, 56, 57	3syl 17	. . . . . . . . . . 11 ⊢ (A ∈ P → ∃z z ∈ (1st ‘A))
59		r19.45mv 3309	. . . . . . . . . . 11 ⊢ (∃z z ∈ (1st ‘A) → (∃z ∈ (1st ‘A)(∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
60	5, 58, 59	3syl 17	. . . . . . . . . 10 ⊢ (A<P B → (∃z ∈ (1st ‘A)(∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
61	60	adantr 261	. . . . . . . . 9 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → (∃z ∈ (1st ‘A)(∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
62		prmu 6460	. . . . . . . . . . . . 13 ⊢ (⟨(1st ‘A), (2nd ‘A)⟩ ∈ P → ∃x ∈ Q x ∈ (2nd ‘A))
63		rexex 2362	. . . . . . . . . . . . 13 ⊢ (∃x ∈ Q x ∈ (2nd ‘A) → ∃x x ∈ (2nd ‘A))
64	6, 62, 63	3syl 17	. . . . . . . . . . . 12 ⊢ (A ∈ P → ∃x x ∈ (2nd ‘A))
65		r19.9rmv 3307	. . . . . . . . . . . . . 14 ⊢ (∃x x ∈ (2nd ‘A) → ((z +Q 𝑟) ∈ (2nd ‘B) ↔ ∃y ∈ (2nd ‘A)(z +Q 𝑟) ∈ (2nd ‘B)))
66	65	orbi2d 703	. . . . . . . . . . . . 13 ⊢ (∃x x ∈ (2nd ‘A) → ((∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃y ∈ (2nd ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
67		r19.43 2462	. . . . . . . . . . . . 13 ⊢ (∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃y ∈ (2nd ‘A)(z +Q 𝑟) ∈ (2nd ‘B)))
68	66, 67	syl6rbbr 188	. . . . . . . . . . . 12 ⊢ (∃x x ∈ (2nd ‘A) → (∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
69	5, 64, 68	3syl 17	. . . . . . . . . . 11 ⊢ (A<P B → (∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
70	69	rexbidv 2321	. . . . . . . . . 10 ⊢ (A<P B → (∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ ∃z ∈ (1st ‘A)(∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
71	70	adantr 261	. . . . . . . . 9 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → (∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ ∃z ∈ (1st ‘A)(∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
72		ibar 285	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ Q → (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
73	72	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q) → (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
74		ibar 285	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ Q → (∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))))
75	74	adantl 262	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q) → (∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)) ↔ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))))
76	73, 75	orbi12d 706	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q) → ((∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ∨ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))) ↔ ((𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))))
77	30, 76	syl 14	. . . . . . . . . . . 12 ⊢ (𝑞 <Q 𝑟 → ((∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ∨ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))) ↔ ((𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))))
78		ltexprlem.1	. . . . . . . . . . . . . 14 ⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩
79	78	ltexprlemell 6571	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
80	78	ltexprlemelu 6572	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
81		eleq1 2097	. . . . . . . . . . . . . . . . 17 ⊢ (y = z → (y ∈ (1st ‘A) ↔ z ∈ (1st ‘A)))
82		oveq1 5462	. . . . . . . . . . . . . . . . . 18 ⊢ (y = z → (y +Q 𝑟) = (z +Q 𝑟))
83	82	eleq1d 2103	. . . . . . . . . . . . . . . . 17 ⊢ (y = z → ((y +Q 𝑟) ∈ (2nd ‘B) ↔ (z +Q 𝑟) ∈ (2nd ‘B)))
84	81, 83	anbi12d 442	. . . . . . . . . . . . . . . 16 ⊢ (y = z → ((y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)) ↔ (z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))
85	84	cbvexv 1792	. . . . . . . . . . . . . . 15 ⊢ (∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)) ↔ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))
86	85	anbi2i 430	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))) ↔ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))
87	80, 86	bitri 173	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))
88	79, 87	orbi12i 680	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ((𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))) ∨ (𝑟 ∈ Q ∧ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))))
89	77, 88	syl6rbbr 188	. . . . . . . . . . 11 ⊢ (𝑞 <Q 𝑟 → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ∨ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))))
90		df-rex 2306	. . . . . . . . . . . 12 ⊢ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ↔ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
91		df-rex 2306	. . . . . . . . . . . 12 ⊢ (∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B) ↔ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B)))
92	90, 91	orbi12i 680	. . . . . . . . . . 11 ⊢ ((∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B)) ↔ (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ∨ ∃z(z ∈ (1st ‘A) ∧ (z +Q 𝑟) ∈ (2nd ‘B))))
93	89, 92	syl6bbr 187	. . . . . . . . . 10 ⊢ (𝑞 <Q 𝑟 → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
94	93	adantl 262	. . . . . . . . 9 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ (∃y ∈ (2nd ‘A)(y +Q 𝑞) ∈ (1st ‘B) ∨ ∃z ∈ (1st ‘A)(z +Q 𝑟) ∈ (2nd ‘B))))
95	61, 71, 94	3bitr4rd 210	. . . . . . . 8 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
96	95	adantr 261	. . . . . . 7 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → ((𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)) ↔ ∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)((y +Q 𝑞) ∈ (1st ‘B) ∨ (z +Q 𝑟) ∈ (2nd ‘B))))
97	55, 96	sylibrd 158	. . . . . 6 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (∃z ∈ (1st ‘A)∃y ∈ (2nd ‘A)y <Q (z +Q w) → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
98	10, 97	mpd 13	. . . . 5 ⊢ (((A<P B ∧ 𝑞 <Q 𝑟) ∧ (w ∈ Q ∧ (𝑞 +Q w) = 𝑟)) → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))
99	2, 98	rexlimddv 2431	. . . 4 ⊢ ((A<P B ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))
100	99	ex 108	. . 3 ⊢ (A<P B → (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
101	100	ralrimivw 2387	. 2 ⊢ (A<P B → ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))
102	101	ralrimivw 2387	1 ⊢ (A<P B → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶))))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  {crab 2304  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1^st c1st 5707  2^nd c2nd 5708  Qcnq 6264   +_Q cplq 6266   <_Q cltq 6269  Pcnp 6275  <_P cltp 6279

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6406  df-nq0 6407  df-0nq0 6408  df-plq0 6409  df-mq0 6410  df-inp 6448  df-iltp 6452

This theorem is referenced by:  ltexprlempr  6581