ltexprlemopl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ltexprlemopl		GIF version

Theorem ltexprlemopl 7409

Description: The lower cut of our constructed difference is open. Lemma for ltexpri 7421. (Contributed by Jim Kingdon, 21-Dec-2019.)

**Hypothesis**
Ref	Expression
ltexprlem.1	⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑥) ∈ (1^st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^st ‘𝐴) ∧ (𝑦 +_Q 𝑥) ∈ (2^nd ‘𝐵))}⟩

**Assertion**
Ref	Expression
ltexprlemopl	⊢ ((𝐴<_P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))

Distinct variable groups: 𝑥,𝑦,𝑞,𝑟,𝐴 𝑥,𝐵,𝑦,𝑞,𝑟 𝑥,𝐶,𝑦,𝑞,𝑟

Proof of Theorem ltexprlemopl Dummy variable 𝑠 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltexprlem.1	. . . . 5 ⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑥) ∈ (1^st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^st ‘𝐴) ∧ (𝑦 +_Q 𝑥) ∈ (2^nd ‘𝐵))}⟩
2	1	ltexprlemell 7406	. . . 4 ⊢ (𝑞 ∈ (1^st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))))
3	2	simprbi 273	. . 3 ⊢ (𝑞 ∈ (1^st ‘𝐶) → ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))
4		19.42v 1878	. . . . . . . 8 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ ∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
5		19.42v 1878	. . . . . . . . 9 ⊢ (∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))))
6	5	anbi2i 452	. . . . . . . 8 ⊢ ((𝐴<_P 𝐵 ∧ ∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
7	4, 6	bitri 183	. . . . . . 7 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
8		ltrelpr 7313	. . . . . . . . . . . . . 14 ⊢ <_P ⊆ (P × P)
9	8	brel 4591	. . . . . . . . . . . . 13 ⊢ (𝐴<_P 𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈ P))
10	9	simprd 113	. . . . . . . . . . . 12 ⊢ (𝐴<_P 𝐵 → 𝐵 ∈ P)
11		prop 7283	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ P → ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P)
12		prnmaxl 7296	. . . . . . . . . . . . 13 ⊢ ((⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
13	11, 12	sylan 281	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ P ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
14	10, 13	sylan 281	. . . . . . . . . . 11 ⊢ ((𝐴<_P 𝐵 ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
15	14	adantrl 469	. . . . . . . . . 10 ⊢ ((𝐴<_P 𝐵 ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
16	15	adantrl 469	. . . . . . . . 9 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
17	9	simpld 111	. . . . . . . . . . . . . . 15 ⊢ (𝐴<_P 𝐵 → 𝐴 ∈ P)
18	17	ad2antrr 479	. . . . . . . . . . . . . 14 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝐴 ∈ P)
19		simplrr 525	. . . . . . . . . . . . . . 15 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))
20	19	simpld 111	. . . . . . . . . . . . . 14 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 ∈ (2^nd ‘𝐴))
21		prop 7283	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ P → ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P)
22		elprnqu 7290	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P ∧ 𝑦 ∈ (2^nd ‘𝐴)) → 𝑦 ∈ Q)
23	21, 22	sylan 281	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ P ∧ 𝑦 ∈ (2^nd ‘𝐴)) → 𝑦 ∈ Q)
24	18, 20, 23	syl2anc 408	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 ∈ Q)
25		simplrl 524	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑞 ∈ Q)
26		ltaddnq 7215	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Q ∧ 𝑞 ∈ Q) → 𝑦 <_Q (𝑦 +_Q 𝑞))
27	24, 25, 26	syl2anc 408	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 <_Q (𝑦 +_Q 𝑞))
28		simprr 521	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 +_Q 𝑞) <_Q 𝑠)
29		ltsonq 7206	. . . . . . . . . . . . 13 ⊢ <_Q Or Q
30		ltrelnq 7173	. . . . . . . . . . . . 13 ⊢ <_Q ⊆ (Q × Q)
31	29, 30	sotri 4934	. . . . . . . . . . . 12 ⊢ ((𝑦 <_Q (𝑦 +_Q 𝑞) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠) → 𝑦 <_Q 𝑠)
32	27, 28, 31	syl2anc 408	. . . . . . . . . . 11 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 <_Q 𝑠)
33	10	ad2antrr 479	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝐵 ∈ P)
34		simprl 520	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑠 ∈ (1^st ‘𝐵))
35		elprnql 7289	. . . . . . . . . . . . . 14 ⊢ ((⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P ∧ 𝑠 ∈ (1^st ‘𝐵)) → 𝑠 ∈ Q)
36	11, 35	sylan 281	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ P ∧ 𝑠 ∈ (1^st ‘𝐵)) → 𝑠 ∈ Q)
37	33, 34, 36	syl2anc 408	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑠 ∈ Q)
38		ltexnqq 7216	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Q ∧ 𝑠 ∈ Q) → (𝑦 <_Q 𝑠 ↔ ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠))
39	24, 37, 38	syl2anc 408	. . . . . . . . . . 11 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 <_Q 𝑠 ↔ ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠))
40	32, 39	mpbid 146	. . . . . . . . . 10 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠)
41		simplrr 525	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑞) <_Q 𝑠)
42		simprr 521	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑟) = 𝑠)
43	41, 42	breqtrrd 3956	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟))
44	25	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑞 ∈ Q)
45		simprl 520	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑟 ∈ Q)
46	24	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑦 ∈ Q)
47		ltanqg 7208	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q ∧ 𝑦 ∈ Q) → (𝑞 <_Q 𝑟 ↔ (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟)))
48	44, 45, 46, 47	syl3anc 1216	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑞 <_Q 𝑟 ↔ (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟)))
49	43, 48	mpbird 166	. . . . . . . . . . . . 13 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑞 <_Q 𝑟)
50	20	adantr 274	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑦 ∈ (2^nd ‘𝐴))
51		simplrl 524	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑠 ∈ (1^st ‘𝐵))
52	42, 51	eqeltrd 2216	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))
53	50, 52	jca 304	. . . . . . . . . . . . 13 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))
54	49, 45, 53	jca32 308	. . . . . . . . . . . 12 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
55	54	expr 372	. . . . . . . . . . 11 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ 𝑟 ∈ Q) → ((𝑦 +_Q 𝑟) = 𝑠 → (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))))
56	55	reximdva 2534	. . . . . . . . . 10 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠 → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))))
57	40, 56	mpd 13	. . . . . . . . 9 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
58	16, 57	rexlimddv 2554	. . . . . . . 8 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
59	58	eximi 1579	. . . . . . 7 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
60	7, 59	sylbir 134	. . . . . 6 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
61		rexcom4 2709	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
62	60, 61	sylibr 133	. . . . 5 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
63		19.42v 1878	. . . . . . 7 ⊢ (∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ ∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
64		19.42v 1878	. . . . . . . 8 ⊢ (∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))
65	64	anbi2i 452	. . . . . . 7 ⊢ ((𝑞 <_Q 𝑟 ∧ ∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
66	63, 65	bitri 183	. . . . . 6 ⊢ (∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
67	66	rexbii 2442	. . . . 5 ⊢ (∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
68	62, 67	sylib 121	. . . 4 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
69	1	ltexprlemell 7406	. . . . . 6 ⊢ (𝑟 ∈ (1^st ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))
70	69	anbi2i 452	. . . . 5 ⊢ ((𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
71	70	rexbii 2442	. . . 4 ⊢ (∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
72	68, 71	sylibr 133	. . 3 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))
73	3, 72	sylanr2 402	. 2 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))
74	73	3impb 1177	1 ⊢ ((𝐴<_P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 962 = wceq 1331 ∃wex 1468 ∈ wcel 1480 ∃wrex 2417 {crab 2420 ⟨cop 3530 class class class wbr 3929 ‘cfv 5123 (class class class)co 5774 1^st c1st 6036 2^nd c2nd 6037 Qcnq 7088 +_Q cplq 7090 <_Q cltq 7093 Pcnp 7099 <_P cltp 7103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-rex 2422 df-reu 2423 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-eprel 4211 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-1o 6313 df-oadd 6317 df-omul 6318 df-er 6429 df-ec 6431 df-qs 6435 df-ni 7112 df-pli 7113 df-mi 7114 df-lti 7115 df-plpq 7152 df-mpq 7153 df-enq 7155 df-nqqs 7156 df-plqqs 7157 df-mqqs 7158 df-1nqqs 7159 df-ltnqqs 7161 df-inp 7274 df-iltp 7278

This theorem is referenced by: ltexprlemrnd 7413

W3C validator