Theorem ltexprlemopu 6567

Description: The upper cut of our constructed difference is open. Lemma for ltexpri 6577. (Contributed by Jim Kingdon, 21-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
ltexprlemopu	⊢ ((A<P B ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))

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

Proof of Theorem ltexprlemopu

Dummy variables 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltexprlem.1	. . . . 5 ⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩
2	1	ltexprlemelu 6563	. . . 4 ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
3	2	simprbi 260	. . 3 ⊢ (𝑟 ∈ (2nd ‘𝐶) → ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))
4		19.42v 1783	. . . . . . . 8 ⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ↔ (A<P B ∧ ∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))))
5		19.42v 1783	. . . . . . . . 9 ⊢ (∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
6	5	anbi2i 430	. . . . . . . 8 ⊢ ((A<P B ∧ ∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ↔ (A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))))
7	4, 6	bitri 173	. . . . . . 7 ⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ↔ (A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))))
8		ltrelpr 6480	. . . . . . . . . . . . . . 15 ⊢ <P ⊆ (P × P)
9	8	brel 4334	. . . . . . . . . . . . . 14 ⊢ (A<P B → (A ∈ P ∧ B ∈ P))
10	9	simprd 107	. . . . . . . . . . . . 13 ⊢ (A<P B → B ∈ P)
11		prop 6450	. . . . . . . . . . . . 13 ⊢ (B ∈ P → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
12	10, 11	syl 14	. . . . . . . . . . . 12 ⊢ (A<P B → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
13		prnminu 6464	. . . . . . . . . . . 12 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ (y +Q 𝑟) ∈ (2nd ‘B)) → ∃𝑠 ∈ (2nd ‘B)𝑠 <Q (y +Q 𝑟))
14	12, 13	sylan 267	. . . . . . . . . . 11 ⊢ ((A<P B ∧ (y +Q 𝑟) ∈ (2nd ‘B)) → ∃𝑠 ∈ (2nd ‘B)𝑠 <Q (y +Q 𝑟))
15	14	adantrl 447	. . . . . . . . . 10 ⊢ ((A<P B ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))) → ∃𝑠 ∈ (2nd ‘B)𝑠 <Q (y +Q 𝑟))
16	15	adantrl 447	. . . . . . . . 9 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃𝑠 ∈ (2nd ‘B)𝑠 <Q (y +Q 𝑟))
17		ltdfpr 6481	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ P ∧ B ∈ P) → (A<P B ↔ ∃𝑡 ∈ Q (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B))))
18	17	biimpd 132	. . . . . . . . . . . . . 14 ⊢ ((A ∈ P ∧ B ∈ P) → (A<P B → ∃𝑡 ∈ Q (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B))))
19	9, 18	mpcom 32	. . . . . . . . . . . . 13 ⊢ (A<P B → ∃𝑡 ∈ Q (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))
20	19	ad2antrr 457	. . . . . . . . . . . 12 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → ∃𝑡 ∈ Q (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))
21	9	simpld 105	. . . . . . . . . . . . . . . 16 ⊢ (A<P B → A ∈ P)
22	21	ad2antrr 457	. . . . . . . . . . . . . . 15 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → A ∈ P)
23	22	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → A ∈ P)
24		simplrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))
25	24	simpld 105	. . . . . . . . . . . . . . 15 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → y ∈ (1st ‘A))
26	25	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → y ∈ (1st ‘A))
27		simprrl 491	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → 𝑡 ∈ (2nd ‘A))
28		prop 6450	. . . . . . . . . . . . . . 15 ⊢ (A ∈ P → ⟨(1st ‘A), (2nd ‘A)⟩ ∈ P)
29		prltlu 6462	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ y ∈ (1st ‘A) ∧ 𝑡 ∈ (2nd ‘A)) → y <Q 𝑡)
30	28, 29	syl3an1 1167	. . . . . . . . . . . . . 14 ⊢ ((A ∈ P ∧ y ∈ (1st ‘A) ∧ 𝑡 ∈ (2nd ‘A)) → y <Q 𝑡)
31	23, 26, 27, 30	syl3anc 1134	. . . . . . . . . . . . 13 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → y <Q 𝑡)
32		simplll 485	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → A<P B)
33		simprrr 492	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → 𝑡 ∈ (1st ‘B))
34		simplrl 487	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → 𝑠 ∈ (2nd ‘B))
35		prltlu 6462	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ 𝑡 ∈ (1st ‘B) ∧ 𝑠 ∈ (2nd ‘B)) → 𝑡 <Q 𝑠)
36	12, 35	syl3an1 1167	. . . . . . . . . . . . . 14 ⊢ ((A<P B ∧ 𝑡 ∈ (1st ‘B) ∧ 𝑠 ∈ (2nd ‘B)) → 𝑡 <Q 𝑠)
37	32, 33, 34, 36	syl3anc 1134	. . . . . . . . . . . . 13 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → 𝑡 <Q 𝑠)
38		ltsonq 6375	. . . . . . . . . . . . . 14 ⊢ <Q Or Q
39		ltrelnq 6342	. . . . . . . . . . . . . 14 ⊢ <Q ⊆ (Q × Q)
40	38, 39	sotri 4662	. . . . . . . . . . . . 13 ⊢ ((y <Q 𝑡 ∧ 𝑡 <Q 𝑠) → y <Q 𝑠)
41	31, 37, 40	syl2anc 391	. . . . . . . . . . . 12 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B)))) → y <Q 𝑠)
42	20, 41	rexlimddv 2431	. . . . . . . . . . 11 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → y <Q 𝑠)
43		elprnql 6456	. . . . . . . . . . . . . 14 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ y ∈ (1st ‘A)) → y ∈ Q)
44	28, 43	sylan 267	. . . . . . . . . . . . 13 ⊢ ((A ∈ P ∧ y ∈ (1st ‘A)) → y ∈ Q)
45	22, 25, 44	syl2anc 391	. . . . . . . . . . . 12 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → y ∈ Q)
46		elprnqu 6457	. . . . . . . . . . . . . 14 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ 𝑠 ∈ (2nd ‘B)) → 𝑠 ∈ Q)
47	12, 46	sylan 267	. . . . . . . . . . . . 13 ⊢ ((A<P B ∧ 𝑠 ∈ (2nd ‘B)) → 𝑠 ∈ Q)
48	47	ad2ant2r 478	. . . . . . . . . . . 12 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → 𝑠 ∈ Q)
49		ltexnqq 6384	. . . . . . . . . . . 12 ⊢ ((y ∈ Q ∧ 𝑠 ∈ Q) → (y <Q 𝑠 ↔ ∃𝑞 ∈ Q (y +Q 𝑞) = 𝑠))
50	45, 48, 49	syl2anc 391	. . . . . . . . . . 11 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → (y <Q 𝑠 ↔ ∃𝑞 ∈ Q (y +Q 𝑞) = 𝑠))
51	42, 50	mpbid 135	. . . . . . . . . 10 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → ∃𝑞 ∈ Q (y +Q 𝑞) = 𝑠)
52		simprr 484	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (y +Q 𝑞) = 𝑠)
53		simplrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → 𝑠 <Q (y +Q 𝑟))
54	52, 53	eqbrtrd 3774	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (y +Q 𝑞) <Q (y +Q 𝑟))
55		simprl 483	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → 𝑞 ∈ Q)
56		simplrl 487	. . . . . . . . . . . . . . . 16 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → 𝑟 ∈ Q)
57	56	adantr 261	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → 𝑟 ∈ Q)
58	45	adantr 261	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → y ∈ Q)
59		ltanqg 6377	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q ∧ y ∈ Q) → (𝑞 <Q 𝑟 ↔ (y +Q 𝑞) <Q (y +Q 𝑟)))
60	55, 57, 58, 59	syl3anc 1134	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (𝑞 <Q 𝑟 ↔ (y +Q 𝑞) <Q (y +Q 𝑟)))
61	54, 60	mpbird 156	. . . . . . . . . . . . 13 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → 𝑞 <Q 𝑟)
62	25	adantr 261	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → y ∈ (1st ‘A))
63		simplrl 487	. . . . . . . . . . . . . . 15 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → 𝑠 ∈ (2nd ‘B))
64	52, 63	eqeltrd 2111	. . . . . . . . . . . . . 14 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (y +Q 𝑞) ∈ (2nd ‘B))
65	62, 64	jca 290	. . . . . . . . . . . . 13 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))
66	61, 55, 65	jca32 293	. . . . . . . . . . . 12 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y +Q 𝑞) = 𝑠)) → (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
67	66	expr 357	. . . . . . . . . . 11 ⊢ ((((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) ∧ 𝑞 ∈ Q) → ((y +Q 𝑞) = 𝑠 → (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B))))))
68	67	reximdva 2415	. . . . . . . . . 10 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → (∃𝑞 ∈ Q (y +Q 𝑞) = 𝑠 → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B))))))
69	51, 68	mpd 13	. . . . . . . . 9 ⊢ (((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) ∧ (𝑠 ∈ (2nd ‘B) ∧ 𝑠 <Q (y +Q 𝑟))) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
70	16, 69	rexlimddv 2431	. . . . . . . 8 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
71	70	eximi 1488	. . . . . . 7 ⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃y∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
72	7, 71	sylbir 125	. . . . . 6 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃y∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
73		rexcom4 2571	. . . . . 6 ⊢ (∃𝑞 ∈ Q ∃y(𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))) ↔ ∃y∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
74	72, 73	sylibr 137	. . . . 5 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃𝑞 ∈ Q ∃y(𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
75		19.42v 1783	. . . . . . 7 ⊢ (∃y(𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))) ↔ (𝑞 <Q 𝑟 ∧ ∃y(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
76		19.42v 1783	. . . . . . . 8 ⊢ (∃y(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B))) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B))))
77	76	anbi2i 430	. . . . . . 7 ⊢ ((𝑞 <Q 𝑟 ∧ ∃y(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))) ↔ (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
78	75, 77	bitri 173	. . . . . 6 ⊢ (∃y(𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))) ↔ (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
79	78	rexbii 2325	. . . . 5 ⊢ (∃𝑞 ∈ Q ∃y(𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
80	74, 79	sylib 127	. . . 4 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
81	1	ltexprlemelu 6563	. . . . . 6 ⊢ (𝑞 ∈ (2nd ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B))))
82	81	anbi2i 430	. . . . 5 ⊢ ((𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) ↔ (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
83	82	rexbii 2325	. . . 4 ⊢ (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈ (2nd ‘B)))))
84	80, 83	sylibr 137	. . 3 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))
85	3, 84	sylanr2 385	. 2 ⊢ ((A<P B ∧ (𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶))) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))
86	85	3impb 1099	1 ⊢ ((A<P B ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃wrex 2301  {crab 2304  ⟨cop 3369   class class class wbr 3754  ‘cfv 4844  (class class class)co 5452  1^st c1st 5704  2^nd c2nd 5705  Qcnq 6257   +_Q cplq 6259   <_Q cltq 6262  Pcnp 6268  <_P cltp 6272

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 3862  ax-sep 3865  ax-nul 3873  ax-pow 3917  ax-pr 3934  ax-un 4135  ax-setind 4219  ax-iinf 4253

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 3352  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-int 3606  df-iun 3649  df-br 3755  df-opab 3809  df-mpt 3810  df-tr 3845  df-eprel 4016  df-id 4020  df-po 4023  df-iso 4024  df-iord 4068  df-on 4070  df-suc 4073  df-iom 4256  df-xp 4293  df-rel 4294  df-cnv 4295  df-co 4296  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-iota 4809  df-fun 4846  df-fn 4847  df-f 4848  df-f1 4849  df-fo 4850  df-f1o 4851  df-fv 4852  df-ov 5455  df-oprab 5456  df-mpt2 5457  df-1st 5706  df-2nd 5707  df-recs 5858  df-irdg 5894  df-1o 5933  df-oadd 5937  df-omul 5938  df-er 6035  df-ec 6037  df-qs 6041  df-ni 6281  df-pli 6282  df-mi 6283  df-lti 6284  df-plpq 6321  df-mpq 6322  df-enq 6324  df-nqqs 6325  df-plqqs 6326  df-mqqs 6327  df-1nqqs 6328  df-ltnqqs 6330  df-inp 6441  df-iltp 6445

This theorem is referenced by:  ltexprlemrnd  6569