caucvgprprlemloc - Intuitionistic Logic Explorer

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

Theorem caucvgprprlemloc 8076

Description: Lemma for caucvgprpr 8085. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.)

**Hypotheses**
Ref	Expression
caucvgprpr.f	⊢ (𝜑 → 𝐹:N⟶P)
caucvgprpr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛)<_P ((𝐹‘𝑘) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩) ∧ (𝐹‘𝑘)<_P ((𝐹‘𝑛) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩))))
caucvgprpr.bnd	⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<_P (𝐹‘𝑚))
caucvgprpr.lim	⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑢}, {𝑞 ∣ 𝑢 <_Q 𝑞}⟩}⟩

**Assertion**
Ref	Expression
caucvgprprlemloc	⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Distinct variable groups: 𝐴,𝑚 𝑚,𝐹 𝐹,𝑙,𝑟 𝑢,𝐹,𝑟 𝑞,𝑝,𝑠,𝑡 𝜑,𝑠,𝑡 𝑝,𝑙,𝑞,𝑠,𝑡,𝑟 𝑢,𝑝,𝑞,𝑠,𝑡 Allowed substitution hints: 𝜑(𝑢, 𝑘, 𝑚, 𝑛, 𝑟, 𝑞, 𝑝, 𝑙) 𝐴(𝑢, 𝑡, 𝑘, 𝑛, 𝑠, 𝑟, 𝑞, 𝑝, 𝑙) 𝐹(𝑡, 𝑘, 𝑛, 𝑠, 𝑞, 𝑝) 𝐿(𝑢, 𝑡, 𝑘, 𝑚, 𝑛, 𝑠, 𝑟, 𝑞, 𝑝, 𝑙)

Proof of Theorem caucvgprprlemloc Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltexnqi 7782	. . . . 5 ⊢ (𝑠 <_Q 𝑡 → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
2	1	adantl 277	. . . 4 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → ∃𝑦 ∈ Q (𝑠 +_Q 𝑦) = 𝑡)
3		subhalfnqq 7787	. . . . . 6 ⊢ (𝑦 ∈ Q → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
4	3	ad2antrl 494	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → ∃𝑥 ∈ Q (𝑥 +_Q 𝑥) <_Q 𝑦)
5		archrecnq 8036	. . . . . . 7 ⊢ (𝑥 ∈ Q → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
6	5	ad2antrl 494	. . . . . 6 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → ∃𝑐 ∈ N (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
7		simpllr 540	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑠 <_Q 𝑡)
8	7	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑠 <_Q 𝑡)
9		simplrl 541	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → 𝑦 ∈ Q)
10	9	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑦 ∈ Q)
11		simplrr 542	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 +_Q 𝑦) = 𝑡)
12	11	adantr 276	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q 𝑦) = 𝑡)
13		simplrl 541	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑥 ∈ Q)
14		simplrr 542	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑥 +_Q 𝑥) <_Q 𝑦)
15		simprl 535	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑐 ∈ N)
16		simprr 537	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)
17	8, 10, 12, 13, 14, 15, 16	caucvgprprlemloccalc 8057	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
18		simplrl 541	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑠 ∈ Q)
19	18	ad3antrrr 496	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑠 ∈ Q)
20		nnnq 7795	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ N → [⟨𝑐, 1_o⟩] ~_Q ∈ Q)
21	20	ad2antrl 494	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → [⟨𝑐, 1_o⟩] ~_Q ∈ Q)
22		recclnq 7765	. . . . . . . . . . . . 13 ⊢ ([⟨𝑐, 1_o⟩] ~_Q ∈ Q → (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
23	21, 22	syl 14	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
24		addclnq 7748	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ Q ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
25	19, 23, 24	syl2anc 415	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
26		nqprlu 7920	. . . . . . . . . . 11 ⊢ ((𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
27	25, 26	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
28		nqprlu 7920	. . . . . . . . . . 11 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
29	23, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
30		addclpr 7910	. . . . . . . . . 10 ⊢ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
31	27, 29, 30	syl2anc 415	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
32		simplrr 542	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → 𝑡 ∈ Q)
33	32	ad3antrrr 496	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝑡 ∈ Q)
34		nqprlu 7920	. . . . . . . . . 10 ⊢ (𝑡 ∈ Q → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
35	33, 34	syl 14	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P)
36		caucvgprpr.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:N⟶P)
37	36	ad5antr 500	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → 𝐹:N⟶P)
38	37, 15	ffvelcdmd 5847	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝐹‘𝑐) ∈ P)
39		ltrelnq 7738	. . . . . . . . . . . . . 14 ⊢ <_Q ⊆ (Q × Q)
40	39	brel 4829	. . . . . . . . . . . . 13 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥 → ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q ∧ 𝑥 ∈ Q))
41	40	simpld 112	. . . . . . . . . . . 12 ⊢ ((_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥 → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
42	41	ad2antll 495	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
43	42, 28	syl 14	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
44		addclpr 7910	. . . . . . . . . 10 ⊢ (((𝐹‘𝑐) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
45	38, 43, 44	syl2anc 415	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)
46		ltsopr 7969	. . . . . . . . . 10 ⊢ <_P Or P
47		sowlin 4467	. . . . . . . . . 10 ⊢ ((<_P Or P ∧ ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
48	46, 47	mpan 428	. . . . . . . . 9 ⊢ (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P ∧ ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ∈ P ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∈ P) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
49	31, 35, 45, 48	syl3anc 1278	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)))
50	17, 49	mpd 13	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
51	19	adantr 276	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ Q)
52		simplrl 541	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑐 ∈ N)
53		simpr 110	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩))
54		ltaprg 7992	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
55	54	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → (𝑓<_P 𝑔 ↔ (ℎ +_P 𝑓)<_P (ℎ +_P 𝑔)))
56	42	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) ∈ Q)
57	51, 56, 24	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) ∈ Q)
58	57, 26	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ ∈ P)
59	38	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (𝐹‘𝑐) ∈ P)
60	56, 28	syl 14	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ ∈ P)
61		addcomprg 7951	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
62	61	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +_P 𝑔) = (𝑔 +_P 𝑓))
63	55, 58, 59, 60, 62	caovord2d 6262	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐) ↔ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)))
64	53, 63	mpbird 167	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐))
65		opeq1 3904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑐 → ⟨𝑎, 1_o⟩ = ⟨𝑐, 1_o⟩)
66	65	eceq1d 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑐 → [⟨𝑎, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
67	66	fveq2d 5702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑐 → (_Q‘[⟨𝑎, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
68	67	oveq2d 6104	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑐 → (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) = (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
69	68	breq2d 4143	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → (𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) ↔ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))))
70	69	abbidv 2358	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))} = {𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))})
71	68	breq1d 4141	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → ((𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞 ↔ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞))
72	71	abbidv 2358	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞} = {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞})
73	70, 72	opeq12d 3912	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩)
74		fveq2 5698	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
75	73, 74	breq12d 4144	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎) ↔ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)))
76	75	rspcev 2929	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑐)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
77	52, 64, 76	syl2anc 415	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (*_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎))
78		caucvgprpr.lim	. . . . . . . . . . 11 ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑙 +_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑟, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑟, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑢}, {𝑞 ∣ 𝑢 <_Q 𝑞}⟩}⟩
79	78	caucvgprprlemell 8058	. . . . . . . . . 10 ⊢ (𝑠 ∈ (1^st ‘𝐿) ↔ (𝑠 ∈ Q ∧ ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑎, 1_o⟩] ~_Q )) <_Q 𝑞}⟩<_P (𝐹‘𝑎)))
80	51, 77, 79	sylanbrc 421	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ (⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)) → 𝑠 ∈ (1^st ‘𝐿))
81	80	ex 115	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → ((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) → 𝑠 ∈ (1^st ‘𝐿)))
82	33	adantr 276	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ Q)
83		fveq2 5698	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐))
84		opeq1 3904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 𝑐 → ⟨𝑏, 1_o⟩ = ⟨𝑐, 1_o⟩)
85	84	eceq1d 6847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → [⟨𝑏, 1_o⟩] ~_Q = [⟨𝑐, 1_o⟩] ~_Q )
86	85	fveq2d 5702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) = (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))
87	86	breq2d 4143	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → (𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) ↔ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )))
88	87	abbidv 2358	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )} = {𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )})
89	86	breq1d 4141	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞 ↔ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞))
90	89	abbidv 2358	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞} = {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞})
91	88, 90	opeq12d 3912	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)
92	83, 91	oveq12d 6106	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑐 → ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) = ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩))
93	92	breq1d 4141	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑐 → (((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ ↔ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
94	93	rspcev 2929	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ N ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
95	15, 94	sylan 283	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩)
96	78	caucvgprprlemelu 8059	. . . . . . . . . 10 ⊢ (𝑡 ∈ (2^nd ‘𝐿) ↔ (𝑡 ∈ Q ∧ ∃𝑏 ∈ N ((𝐹‘𝑏) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑏, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑏, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩))
97	82, 95, 96	sylanbrc 421	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) ∧ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → 𝑡 ∈ (2^nd ‘𝐿))
98	97	ex 115	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩ → 𝑡 ∈ (2^nd ‘𝐿)))
99	81, 98	orim12d 798	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (((⟨{𝑝 ∣ 𝑝 <_Q (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q ))}, {𝑞 ∣ (𝑠 +_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )) <_Q 𝑞}⟩ +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩) ∨ ((𝐹‘𝑐) +_P ⟨{𝑝 ∣ 𝑝 <_Q (_Q‘[⟨𝑐, 1_o⟩] ~_Q )}, {𝑞 ∣ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑞}⟩)<_P ⟨{𝑝 ∣ 𝑝 <_Q 𝑡}, {𝑞 ∣ 𝑡 <_Q 𝑞}⟩) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
100	50, 99	mpd 13	. . . . . 6 ⊢ ((((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) ∧ (𝑐 ∈ N ∧ (*_Q‘[⟨𝑐, 1_o⟩] ~_Q ) <_Q 𝑥)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
101	6, 100	rexlimddv 2673	. . . . 5 ⊢ (((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) ∧ (𝑥 ∈ Q ∧ (𝑥 +_Q 𝑥) <_Q 𝑦)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
102	4, 101	rexlimddv 2673	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) ∧ (𝑦 ∈ Q ∧ (𝑠 +_Q 𝑦) = 𝑡)) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
103	2, 102	rexlimddv 2673	. . 3 ⊢ (((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) ∧ 𝑠 <_Q 𝑡) → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿)))
104	103	ex 115	. 2 ⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))
105	104	ralrimivva 2632	1 ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <_Q 𝑡 → (𝑠 ∈ (1^st ‘𝐿) ∨ 𝑡 ∈ (2^nd ‘𝐿))))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 {cab 2224 ∀wral 2528 ∃wrex 2529 {crab 2532 ⟨cop 3712 class class class wbr 4131 Or wor 4442 ⟶wf 5376 ‘cfv 5380 (class class class)co 6088 1^st c1st 6376 2^nd c2nd 6377 1_oc1o 6684 [cec 6809 Ncnpi 7645 <_N clti 7648 ~_Q ceq 7652 Qcnq 7653 +_Q cplq 7655 *_Qcrq 7657 <_Q cltq 7658 Pcnp 7664 +_P cpp 7666 <_P cltp 7668

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-eprel 4436 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-1o 6691 df-2o 6692 df-oadd 6695 df-omul 6696 df-er 6811 df-ec 6813 df-qs 6817 df-ni 7677 df-pli 7678 df-mi 7679 df-lti 7680 df-plpq 7717 df-mpq 7718 df-enq 7720 df-nqqs 7721 df-plqqs 7722 df-mqqs 7723 df-1nqqs 7724 df-rq 7725 df-ltnqqs 7726 df-enq0 7797 df-nq0 7798 df-0nq0 7799 df-plq0 7800 df-mq0 7801 df-inp 7839 df-iplp 7841 df-iltp 7843

This theorem is used by: caucvgprprlemcl 8077

W3C validator