Theorem ltexprlemm 6431

Description: Our constructed difference is inhabited. Lemma for ltexpri 6444. (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
ltexprlemm	⊢ (A<P B → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)))

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

Proof of Theorem ltexprlemm

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelpr 6353	. . . . . . . . 9 ⊢ <P ⊆ (P × P)
2	1	brel 4315	. . . . . . . 8 ⊢ (A<P B → (A ∈ P ∧ B ∈ P))
3		ltdfpr 6354	. . . . . . . . 9 ⊢ ((A ∈ P ∧ B ∈ P) → (A<P B ↔ ∃y ∈ Q (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B))))
4	3	biimpd 132	. . . . . . . 8 ⊢ ((A ∈ P ∧ B ∈ P) → (A<P B → ∃y ∈ Q (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B))))
5	2, 4	mpcom 32	. . . . . . 7 ⊢ (A<P B → ∃y ∈ Q (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)))
6		simprrl 479	. . . . . . . . . 10 ⊢ ((A<P B ∧ (y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)))) → y ∈ (2nd ‘A))
7	2	simprd 107	. . . . . . . . . . . . 13 ⊢ (A<P B → B ∈ P)
8		prop 6323	. . . . . . . . . . . . . . . . . 18 ⊢ (B ∈ P → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
9		prnmaxl 6336	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)y <Q w)
10	8, 9	sylan 267	. . . . . . . . . . . . . . . . 17 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)y <Q w)
11		ltrelnq 6218	. . . . . . . . . . . . . . . . . . . 20 ⊢ <Q ⊆ (Q × Q)
12	11	brel 4315	. . . . . . . . . . . . . . . . . . 19 ⊢ (y <Q w → (y ∈ Q ∧ w ∈ Q))
13		ltexnqq 6260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ Q ∧ w ∈ Q) → (y <Q w ↔ ∃𝑞 ∈ Q (y +Q 𝑞) = w))
14	13	biimpd 132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ Q ∧ w ∈ Q) → (y <Q w → ∃𝑞 ∈ Q (y +Q 𝑞) = w))
15	12, 14	mpcom 32	. . . . . . . . . . . . . . . . . 18 ⊢ (y <Q w → ∃𝑞 ∈ Q (y +Q 𝑞) = w)
16	15	reximi 2390	. . . . . . . . . . . . . . . . 17 ⊢ (∃w ∈ (1st ‘B)y <Q w → ∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w)
17	10, 16	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w)
18		df-rex 2286	. . . . . . . . . . . . . . . 16 ⊢ (∃w ∈ (1st ‘B)∃𝑞 ∈ Q (y +Q 𝑞) = w ↔ ∃w(w ∈ (1st ‘B) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) = w))
19	17, 18	sylib 127	. . . . . . . . . . . . . . 15 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w(w ∈ (1st ‘B) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) = w))
20		r19.42v 2441	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑞 ∈ Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w) ↔ (w ∈ (1st ‘B) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) = w))
21	20	exbii 1474	. . . . . . . . . . . . . . 15 ⊢ (∃w∃𝑞 ∈ Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w) ↔ ∃w(w ∈ (1st ‘B) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) = w))
22	19, 21	sylibr 137	. . . . . . . . . . . . . 14 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → ∃w∃𝑞 ∈ Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w))
23		eleq1 2078	. . . . . . . . . . . . . . . . 17 ⊢ ((y +Q 𝑞) = w → ((y +Q 𝑞) ∈ (1st ‘B) ↔ w ∈ (1st ‘B)))
24	23	biimparc 283	. . . . . . . . . . . . . . . 16 ⊢ ((w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w) → (y +Q 𝑞) ∈ (1st ‘B))
25	24	reximi 2390	. . . . . . . . . . . . . . 15 ⊢ (∃𝑞 ∈ Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
26	25	exlimiv 1467	. . . . . . . . . . . . . 14 ⊢ (∃w∃𝑞 ∈ Q (w ∈ (1st ‘B) ∧ (y +Q 𝑞) = w) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
27	22, 26	syl 14	. . . . . . . . . . . . 13 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
28	7, 27	sylan 267	. . . . . . . . . . . 12 ⊢ ((A<P B ∧ y ∈ (1st ‘B)) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
29	28	adantrl 450	. . . . . . . . . . 11 ⊢ ((A<P B ∧ (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B))) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
30	29	adantrl 450	. . . . . . . . . 10 ⊢ ((A<P B ∧ (y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)))) → ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))
31	6, 30	jca 290	. . . . . . . . 9 ⊢ ((A<P B ∧ (y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)))) → (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B)))
32	31	expr 357	. . . . . . . 8 ⊢ ((A<P B ∧ y ∈ Q) → ((y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)) → (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))))
33	32	reximdva 2395	. . . . . . 7 ⊢ (A<P B → (∃y ∈ Q (y ∈ (2nd ‘A) ∧ y ∈ (1st ‘B)) → ∃y ∈ Q (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B))))
34	5, 33	mpd 13	. . . . . 6 ⊢ (A<P B → ∃y ∈ Q (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B)))
35		r19.42v 2441	. . . . . . 7 ⊢ (∃𝑞 ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B)))
36	35	rexbii 2305	. . . . . 6 ⊢ (∃y ∈ Q ∃𝑞 ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃y ∈ Q (y ∈ (2nd ‘A) ∧ ∃𝑞 ∈ Q (y +Q 𝑞) ∈ (1st ‘B)))
37	34, 36	sylibr 137	. . . . 5 ⊢ (A<P B → ∃y ∈ Q ∃𝑞 ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
38		rexcom 2448	. . . . 5 ⊢ (∃y ∈ Q ∃𝑞 ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
39	37, 38	sylib 127	. . . 4 ⊢ (A<P B → ∃𝑞 ∈ Q ∃y ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
40	2	simpld 105	. . . . . . . . . . . 12 ⊢ (A<P B → A ∈ P)
41		prop 6323	. . . . . . . . . . . . 13 ⊢ (A ∈ P → ⟨(1st ‘A), (2nd ‘A)⟩ ∈ P)
42		elprnqu 6330	. . . . . . . . . . . . 13 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ y ∈ (2nd ‘A)) → y ∈ Q)
43	41, 42	sylan 267	. . . . . . . . . . . 12 ⊢ ((A ∈ P ∧ y ∈ (2nd ‘A)) → y ∈ Q)
44	40, 43	sylan 267	. . . . . . . . . . 11 ⊢ ((A<P B ∧ y ∈ (2nd ‘A)) → y ∈ Q)
45	44	ex 108	. . . . . . . . . 10 ⊢ (A<P B → (y ∈ (2nd ‘A) → y ∈ Q))
46	45	pm4.71rd 374	. . . . . . . . 9 ⊢ (A<P B → (y ∈ (2nd ‘A) ↔ (y ∈ Q ∧ y ∈ (2nd ‘A))))
47	46	anbi1d 441	. . . . . . . 8 ⊢ (A<P B → ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ((y ∈ Q ∧ y ∈ (2nd ‘A)) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
48		anass 383	. . . . . . . 8 ⊢ (((y ∈ Q ∧ y ∈ (2nd ‘A)) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ (y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
49	47, 48	syl6bb 185	. . . . . . 7 ⊢ (A<P B → ((y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ (y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
50	49	exbidv 1684	. . . . . 6 ⊢ (A<P B → (∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃y(y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
51	50	rexbidv 2301	. . . . 5 ⊢ (A<P B → (∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y(y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
52		df-rex 2286	. . . . . 6 ⊢ (∃y ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃y(y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
53	52	rexbii 2305	. . . . 5 ⊢ (∃𝑞 ∈ Q ∃y ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y(y ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
54	51, 53	syl6bbr 187	. . . 4 ⊢ (A<P B → (∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q ∃y ∈ Q (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
55	39, 54	mpbird 156	. . 3 ⊢ (A<P B → ∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
56		ltexprlem.1	. . . . . 6 ⊢ 𝐶 = ⟨{x ∈ Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈ (1st ‘B))}, {x ∈ Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈ (2nd ‘B))}⟩
57	56	ltexprlemell 6429	. . . . 5 ⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
58	57	rexbii 2305	. . . 4 ⊢ (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
59		ssid 2937	. . . . 5 ⊢ Q ⊆ Q
60		rexss 2980	. . . . 5 ⊢ (Q ⊆ Q → (∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))))
61	59, 60	ax-mp 7	. . . 4 ⊢ (∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)) ↔ ∃𝑞 ∈ Q (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B))))
62	58, 61	bitr4i 176	. . 3 ⊢ (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑞 ∈ Q ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈ (1st ‘B)))
63	55, 62	sylibr 137	. 2 ⊢ (A<P B → ∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶))
64		nfv 1398	. . 3 ⊢ Ⅎ𝑟 A<P B
65		nfre1 2339	. . 3 ⊢ Ⅎ𝑟∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)
66		prmu 6326	. . . . 5 ⊢ (⟨(1st ‘B), (2nd ‘B)⟩ ∈ P → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘B))
67		rexex 2342	. . . . 5 ⊢ (∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘B) → ∃𝑟 𝑟 ∈ (2nd ‘B))
68	66, 67	syl 14	. . . 4 ⊢ (⟨(1st ‘B), (2nd ‘B)⟩ ∈ P → ∃𝑟 𝑟 ∈ (2nd ‘B))
69	7, 8, 68	3syl 17	. . 3 ⊢ (A<P B → ∃𝑟 𝑟 ∈ (2nd ‘B))
70		elprnqu 6330	. . . . . . 7 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈ Q)
71	8, 70	sylan 267	. . . . . 6 ⊢ ((B ∈ P ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈ Q)
72	7, 71	sylan 267	. . . . 5 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈ Q)
73		prml 6325	. . . . . . . . 9 ⊢ (⟨(1st ‘A), (2nd ‘A)⟩ ∈ P → ∃y ∈ Q y ∈ (1st ‘A))
74	41, 73	syl 14	. . . . . . . 8 ⊢ (A ∈ P → ∃y ∈ Q y ∈ (1st ‘A))
75		rexex 2342	. . . . . . . 8 ⊢ (∃y ∈ Q y ∈ (1st ‘A) → ∃y y ∈ (1st ‘A))
76	40, 74, 75	3syl 17	. . . . . . 7 ⊢ (A<P B → ∃y y ∈ (1st ‘A))
77	76	adantr 261	. . . . . 6 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → ∃y y ∈ (1st ‘A))
78	72	3adant3 910	. . . . . . . . 9 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → 𝑟 ∈ Q)
79		simp3 892	. . . . . . . . . 10 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → y ∈ (1st ‘A))
80		elprnql 6329	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ y ∈ (1st ‘A)) → y ∈ Q)
81	41, 80	sylan 267	. . . . . . . . . . . . . 14 ⊢ ((A ∈ P ∧ y ∈ (1st ‘A)) → y ∈ Q)
82	40, 81	sylan 267	. . . . . . . . . . . . 13 ⊢ ((A<P B ∧ y ∈ (1st ‘A)) → y ∈ Q)
83	82	3adant2 909	. . . . . . . . . . . 12 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → y ∈ Q)
84		addcomnqg 6234	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ Q ∧ y ∈ Q) → (𝑟 +Q y) = (y +Q 𝑟))
85	78, 83, 84	syl2anc 393	. . . . . . . . . . 11 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → (𝑟 +Q y) = (y +Q 𝑟))
86		ltaddnq 6259	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ Q ∧ y ∈ Q) → 𝑟 <Q (𝑟 +Q y))
87	78, 83, 86	syl2anc 393	. . . . . . . . . . . 12 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → 𝑟 <Q (𝑟 +Q y))
88		prcunqu 6333	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ 𝑟 ∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q y) → (𝑟 +Q y) ∈ (2nd ‘B)))
89	8, 88	sylan 267	. . . . . . . . . . . . . 14 ⊢ ((B ∈ P ∧ 𝑟 ∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q y) → (𝑟 +Q y) ∈ (2nd ‘B)))
90	7, 89	sylan 267	. . . . . . . . . . . . 13 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → (𝑟 <Q (𝑟 +Q y) → (𝑟 +Q y) ∈ (2nd ‘B)))
91	90	3adant3 910	. . . . . . . . . . . 12 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → (𝑟 <Q (𝑟 +Q y) → (𝑟 +Q y) ∈ (2nd ‘B)))
92	87, 91	mpd 13	. . . . . . . . . . 11 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → (𝑟 +Q y) ∈ (2nd ‘B))
93	85, 92	eqeltrrd 2093	. . . . . . . . . 10 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → (y +Q 𝑟) ∈ (2nd ‘B))
94		19.8a 1460	. . . . . . . . . 10 ⊢ ((y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)) → ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))
95	79, 93, 94	syl2anc 393	. . . . . . . . 9 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B)))
96	78, 95	jca 290	. . . . . . . 8 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
97	56	ltexprlemelu 6430	. . . . . . . 8 ⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈ (2nd ‘B))))
98	96, 97	sylibr 137	. . . . . . 7 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B) ∧ y ∈ (1st ‘A)) → 𝑟 ∈ (2nd ‘𝐶))
99	98	3expa 1088	. . . . . 6 ⊢ (((A<P B ∧ 𝑟 ∈ (2nd ‘B)) ∧ y ∈ (1st ‘A)) → 𝑟 ∈ (2nd ‘𝐶))
100	77, 99	exlimddv 1756	. . . . 5 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → 𝑟 ∈ (2nd ‘𝐶))
101		19.8a 1460	. . . . 5 ⊢ ((𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑟(𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)))
102	72, 100, 101	syl2anc 393	. . . 4 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑟(𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)))
103		df-rex 2286	. . . 4 ⊢ (∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑟(𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)))
104	102, 103	sylibr 137	. . 3 ⊢ ((A<P B ∧ 𝑟 ∈ (2nd ‘B)) → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶))
105	64, 65, 69, 104	exlimdd 1730	. 2 ⊢ (A<P B → ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶))
106	63, 105	jca 290	1 ⊢ (A<P B → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 871   = wceq 1226  ∃wex 1358   ∈ wcel 1370  ∃wrex 2281  {crab 2284   ⊆ wss 2890  ⟨cop 3349   class class class wbr 3734  ‘cfv 4825  (class class class)co 5432  1^st c1st 5684  2^nd c2nd 5685  Qcnq 6134   +_Q cplq 6136   <_Q cltq 6139  Pcnp 6145  <_P cltp 6149

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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-coll 3842  ax-sep 3845  ax-nul 3853  ax-pow 3897  ax-pr 3914  ax-un 4116  ax-setind 4200  ax-iinf 4234

This theorem depends on definitions:  df-bi 110  df-dc 731  df-3or 872  df-3an 873  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-rex 2286  df-reu 2287  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-int 3586  df-iun 3629  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-eprel 3996  df-id 4000  df-iord 4048  df-on 4050  df-suc 4053  df-iom 4237  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833  df-ov 5435  df-oprab 5436  df-mpt2 5437  df-1st 5686  df-2nd 5687  df-recs 5838  df-irdg 5874  df-1o 5912  df-oadd 5916  df-omul 5917  df-er 6013  df-ec 6015  df-qs 6019  df-ni 6158  df-pli 6159  df-mi 6160  df-lti 6161  df-plpq 6197  df-mpq 6198  df-enq 6200  df-nqqs 6201  df-plqqs 6202  df-mqqs 6203  df-1nqqs 6204  df-ltnqqs 6206  df-inp 6314  df-iltp 6318

This theorem is referenced by:  ltexprlempr  6439