ltexprlemopl - Intuitionistic Logic Explorer

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

Theorem ltexprlemopl 7618

Description: The lower cut of our constructed difference is open. Lemma for ltexpri 7630. (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 7615	. . . 4 ⊢ (𝑞 ∈ (1^st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))))
3	2	simprbi 275	. . 3 ⊢ (𝑞 ∈ (1^st ‘𝐶) → ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))
4		19.42v 1918	. . . . . . . 8 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ ∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
5		19.42v 1918	. . . . . . . . 9 ⊢ (∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))))
6	5	anbi2i 457	. . . . . . . 8 ⊢ ((𝐴<_P 𝐵 ∧ ∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
7	4, 6	bitri 184	. . . . . . 7 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
8		ltrelpr 7522	. . . . . . . . . . . . . 14 ⊢ <_P ⊆ (P × P)
9	8	brel 4693	. . . . . . . . . . . . 13 ⊢ (𝐴<_P 𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈ P))
10	9	simprd 114	. . . . . . . . . . . 12 ⊢ (𝐴<_P 𝐵 → 𝐵 ∈ P)
11		prop 7492	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ P → ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P)
12		prnmaxl 7505	. . . . . . . . . . . . 13 ⊢ ((⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
13	11, 12	sylan 283	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ P ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
14	10, 13	sylan 283	. . . . . . . . . . 11 ⊢ ((𝐴<_P 𝐵 ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
15	14	adantrl 478	. . . . . . . . . 10 ⊢ ((𝐴<_P 𝐵 ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
16	15	adantrl 478	. . . . . . . . 9 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑠 ∈ (1^st ‘𝐵)(𝑦 +_Q 𝑞) <_Q 𝑠)
17	9	simpld 112	. . . . . . . . . . . . . . 15 ⊢ (𝐴<_P 𝐵 → 𝐴 ∈ P)
18	17	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝐴 ∈ P)
19		simplrr 536	. . . . . . . . . . . . . . 15 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))
20	19	simpld 112	. . . . . . . . . . . . . 14 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 ∈ (2^nd ‘𝐴))
21		prop 7492	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ P → ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P)
22		elprnqu 7499	. . . . . . . . . . . . . . 15 ⊢ ((⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P ∧ 𝑦 ∈ (2^nd ‘𝐴)) → 𝑦 ∈ Q)
23	21, 22	sylan 283	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ P ∧ 𝑦 ∈ (2^nd ‘𝐴)) → 𝑦 ∈ Q)
24	18, 20, 23	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 ∈ Q)
25		simplrl 535	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑞 ∈ Q)
26		ltaddnq 7424	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Q ∧ 𝑞 ∈ Q) → 𝑦 <_Q (𝑦 +_Q 𝑞))
27	24, 25, 26	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 <_Q (𝑦 +_Q 𝑞))
28		simprr 531	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 +_Q 𝑞) <_Q 𝑠)
29		ltsonq 7415	. . . . . . . . . . . . 13 ⊢ <_Q Or Q
30		ltrelnq 7382	. . . . . . . . . . . . 13 ⊢ <_Q ⊆ (Q × Q)
31	29, 30	sotri 5039	. . . . . . . . . . . 12 ⊢ ((𝑦 <_Q (𝑦 +_Q 𝑞) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠) → 𝑦 <_Q 𝑠)
32	27, 28, 31	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑦 <_Q 𝑠)
33	10	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝐵 ∈ P)
34		simprl 529	. . . . . . . . . . . . 13 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑠 ∈ (1^st ‘𝐵))
35		elprnql 7498	. . . . . . . . . . . . . 14 ⊢ ((⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P ∧ 𝑠 ∈ (1^st ‘𝐵)) → 𝑠 ∈ Q)
36	11, 35	sylan 283	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ P ∧ 𝑠 ∈ (1^st ‘𝐵)) → 𝑠 ∈ Q)
37	33, 34, 36	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → 𝑠 ∈ Q)
38		ltexnqq 7425	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Q ∧ 𝑠 ∈ Q) → (𝑦 <_Q 𝑠 ↔ ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠))
39	24, 37, 38	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → (𝑦 <_Q 𝑠 ↔ ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠))
40	32, 39	mpbid 147	. . . . . . . . . 10 ⊢ (((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) → ∃𝑟 ∈ Q (𝑦 +_Q 𝑟) = 𝑠)
41		simplrr 536	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑞) <_Q 𝑠)
42		simprr 531	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑟) = 𝑠)
43	41, 42	breqtrrd 4046	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟))
44	25	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑞 ∈ Q)
45		simprl 529	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑟 ∈ Q)
46	24	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑦 ∈ Q)
47		ltanqg 7417	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q ∧ 𝑦 ∈ Q) → (𝑞 <_Q 𝑟 ↔ (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟)))
48	44, 45, 46, 47	syl3anc 1249	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑞 <_Q 𝑟 ↔ (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟)))
49	43, 48	mpbird 167	. . . . . . . . . . . . 13 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑞 <_Q 𝑟)
50	20	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑦 ∈ (2^nd ‘𝐴))
51		simplrl 535	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → 𝑠 ∈ (1^st ‘𝐵))
52	42, 51	eqeltrd 2266	. . . . . . . . . . . . . 14 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))
53	50, 52	jca 306	. . . . . . . . . . . . 13 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))
54	49, 45, 53	jca32 310	. . . . . . . . . . . 12 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ (𝑟 ∈ Q ∧ (𝑦 +_Q 𝑟) = 𝑠)) → (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
55	54	expr 375	. . . . . . . . . . 11 ⊢ ((((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ∧ (𝑠 ∈ (1^st ‘𝐵) ∧ (𝑦 +_Q 𝑞) <_Q 𝑠)) ∧ 𝑟 ∈ Q) → ((𝑦 +_Q 𝑟) = 𝑠 → (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))))
56	55	reximdva 2592	. . . . . . . . . 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 2612	. . . . . . . 8 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
59	58	eximi 1611	. . . . . . 7 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
60	7, 59	sylbir 135	. . . . . 6 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
61		rexcom4 2775	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ ∃𝑦∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
62	60, 61	sylibr 134	. . . . 5 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
63		19.42v 1918	. . . . . . 7 ⊢ (∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ ∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
64		19.42v 1918	. . . . . . . 8 ⊢ (∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))
65	64	anbi2i 457	. . . . . . 7 ⊢ ((𝑞 <_Q 𝑟 ∧ ∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
66	63, 65	bitri 184	. . . . . 6 ⊢ (∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
67	66	rexbii 2497	. . . . 5 ⊢ (∃𝑟 ∈ Q ∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
68	62, 67	sylib 122	. . . 4 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
69	1	ltexprlemell 7615	. . . . . 6 ⊢ (𝑟 ∈ (1^st ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵))))
70	69	anbi2i 457	. . . . 5 ⊢ ((𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)) ↔ (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
71	70	rexbii 2497	. . . 4 ⊢ (∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)) ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
72	68, 71	sylibr 134	. . 3 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))
73	3, 72	sylanr2 405	. 2 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))
74	73	3impb 1201	1 ⊢ ((𝐴<_P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∃wex 1503 ∈ wcel 2160 ∃wrex 2469 {crab 2472 ⟨cop 3610 class class class wbr 4018 ‘cfv 5231 (class class class)co 5891 1^st c1st 6157 2^nd c2nd 6158 Qcnq 7297 +_Q cplq 7299 <_Q cltq 7302 Pcnp 7308 <_P cltp 7312

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-eprel 4304 df-id 4308 df-po 4311 df-iso 4312 df-iord 4381 df-on 4383 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5233 df-fn 5234 df-f 5235 df-f1 5236 df-fo 5237 df-f1o 5238 df-fv 5239 df-ov 5894 df-oprab 5895 df-mpo 5896 df-1st 6159 df-2nd 6160 df-recs 6324 df-irdg 6389 df-1o 6435 df-oadd 6439 df-omul 6440 df-er 6553 df-ec 6555 df-qs 6559 df-ni 7321 df-pli 7322 df-mi 7323 df-lti 7324 df-plpq 7361 df-mpq 7362 df-enq 7364 df-nqqs 7365 df-plqqs 7366 df-mqqs 7367 df-1nqqs 7368 df-ltnqqs 7370 df-inp 7483 df-iltp 7487

This theorem is referenced by: ltexprlemrnd 7622

W3C validator