ltexprlemopl - Intuitionistic Logic Explorer

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

Theorem ltexprlemopl 7595

Description: The lower cut of our constructed difference is open. Lemma for ltexpri 7607. (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 7592	. . . 4 ⊢ (𝑞 ∈ (1^st ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵))))
3	2	simprbi 275	. . 3 ⊢ (𝑞 ∈ (1^st ‘𝐶) → ∃𝑦(𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))
4		19.42v 1906	. . . . . . . 8 ⊢ (∃𝑦(𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) ↔ (𝐴<_P 𝐵 ∧ ∃𝑦(𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))))
5		19.42v 1906	. . . . . . . . 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 7499	. . . . . . . . . . . . . 14 ⊢ <_P ⊆ (P × P)
9	8	brel 4676	. . . . . . . . . . . . 13 ⊢ (𝐴<_P 𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈ P))
10	9	simprd 114	. . . . . . . . . . . 12 ⊢ (𝐴<_P 𝐵 → 𝐵 ∈ P)
11		prop 7469	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ P → ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P)
12		prnmaxl 7482	. . . . . . . . . . . . 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 7469	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ P → ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P)
22		elprnqu 7476	. . . . . . . . . . . . . . 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 7401	. . . . . . . . . . . . 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 7392	. . . . . . . . . . . . 13 ⊢ <_Q Or Q
30		ltrelnq 7359	. . . . . . . . . . . . 13 ⊢ <_Q ⊆ (Q × Q)
31	29, 30	sotri 5021	. . . . . . . . . . . 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 7475	. . . . . . . . . . . . . 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 7402	. . . . . . . . . . . 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 4029	. . . . . . . . . . . . . 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 7394	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ Q ∧ 𝑟 ∈ Q ∧ 𝑦 ∈ Q) → (𝑞 <_Q 𝑟 ↔ (𝑦 +_Q 𝑞) <_Q (𝑦 +_Q 𝑟)))
48	44, 45, 46, 47	syl3anc 1238	. . . . . . . . . . . . . 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 2254	. . . . . . . . . . . . . 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 2579	. . . . . . . . . 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 2599	. . . . . . . 8 ⊢ ((𝐴<_P 𝐵 ∧ (𝑞 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑞) ∈ (1^st ‘𝐵)))) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
59	58	eximi 1600	. . . . . . 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 2760	. . . . . 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 1906	. . . . . . 7 ⊢ (∃𝑦(𝑞 <_Q 𝑟 ∧ (𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))) ↔ (𝑞 <_Q 𝑟 ∧ ∃𝑦(𝑟 ∈ Q ∧ (𝑦 ∈ (2^nd ‘𝐴) ∧ (𝑦 +_Q 𝑟) ∈ (1^st ‘𝐵)))))
64		19.42v 1906	. . . . . . . 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 2484	. . . . 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 7592	. . . . . 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 2484	. . . 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 1199	1 ⊢ ((𝐴<_P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐶)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ∃wrex 2456 {crab 2459 ⟨cop 3595 class class class wbr 4001 ‘cfv 5213 (class class class)co 5870 1^st c1st 6134 2^nd c2nd 6135 Qcnq 7274 +_Q cplq 7276 <_Q cltq 7279 Pcnp 7285 <_P cltp 7289

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4116 ax-sep 4119 ax-nul 4127 ax-pow 4172 ax-pr 4207 ax-un 4431 ax-setind 4534 ax-iinf 4585

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3809 df-int 3844 df-iun 3887 df-br 4002 df-opab 4063 df-mpt 4064 df-tr 4100 df-eprel 4287 df-id 4291 df-po 4294 df-iso 4295 df-iord 4364 df-on 4366 df-suc 4369 df-iom 4588 df-xp 4630 df-rel 4631 df-cnv 4632 df-co 4633 df-dm 4634 df-rn 4635 df-res 4636 df-ima 4637 df-iota 5175 df-fun 5215 df-fn 5216 df-f 5217 df-f1 5218 df-fo 5219 df-f1o 5220 df-fv 5221 df-ov 5873 df-oprab 5874 df-mpo 5875 df-1st 6136 df-2nd 6137 df-recs 6301 df-irdg 6366 df-1o 6412 df-oadd 6416 df-omul 6417 df-er 6530 df-ec 6532 df-qs 6536 df-ni 7298 df-pli 7299 df-mi 7300 df-lti 7301 df-plpq 7338 df-mpq 7339 df-enq 7341 df-nqqs 7342 df-plqqs 7343 df-mqqs 7344 df-1nqqs 7345 df-ltnqqs 7347 df-inp 7460 df-iltp 7464

This theorem is referenced by: ltexprlemrnd 7599

W3C validator