caucvgsrlemgt1 - Intuitionistic Logic Explorer

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

Theorem caucvgsrlemgt1 8152

Description: Lemma for caucvgsr 8159. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.)

**Hypotheses**
Ref	Expression
caucvgsr.f	⊢ (𝜑 → 𝐹:N⟶R)
caucvgsr.cau	⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_R ((𝐹‘𝑘) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ) ∧ (𝐹‘𝑘) <_R ((𝐹‘𝑛) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))))
caucvgsrlemgt1.gt1	⊢ (𝜑 → ∀𝑚 ∈ N 1_R <_R (𝐹‘𝑚))

**Assertion**
Ref	Expression
caucvgsrlemgt1	⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))

Distinct variable groups: 𝑗,𝐹,𝑘,𝑙,𝑢 𝑖,𝐹,𝑥,𝑗,𝑘 𝑚,𝐹,𝑛,𝑘 𝑛,𝑙,𝑢 𝑦,𝐹,𝑖,𝑗,𝑥 𝜑,𝑗,𝑘,𝑥 𝜑,𝑛 𝑘,𝑚,𝑛 Allowed substitution hints: 𝜑(𝑦,𝑢,𝑖,𝑚,𝑙)

Proof of Theorem caucvgsrlemgt1 Dummy variables 𝑎 𝑏 𝑤 𝑧 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		caucvgsr.f	. . . 4 ⊢ (𝜑 → 𝐹:N⟶R)
2		caucvgsr.cau	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → ((𝐹‘𝑛) <_R ((𝐹‘𝑘) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ) ∧ (𝐹‘𝑘) <_R ((𝐹‘𝑛) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))))
3		caucvgsrlemgt1.gt1	. . . 4 ⊢ (𝜑 → ∀𝑚 ∈ N 1_R <_R (𝐹‘𝑚))
4		eqid 2238	. . . 4 ⊢ (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )) = (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))
5	1, 2, 3, 4	caucvgsrlemf 8149	. . 3 ⊢ (𝜑 → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
6	1, 2, 3, 4	caucvgsrlemcau 8150	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑛)<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩) ∧ ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑛) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_o⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_o⟩] ~_Q ) <_Q 𝑢}⟩))))
7	1, 2, 3, 4	caucvgsrlembound 8151	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ N 1_P<_P ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑚))
8	5, 6, 7	caucvgprpr 8069	. 2 ⊢ (𝜑 → ∃𝑎 ∈ P ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))
9		prsrcl 8141	. . . 4 ⊢ (𝑎 ∈ P → [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R)
10	9	ad2antrl 494	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) → [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R)
11		oveq2 6083	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎 +_P 𝑏) = (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
12	11	breq2d 4137	. . . . . . . . . . 11 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ↔ ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥))))
13		oveq2 6083	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏) = (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
14	13	breq2d 4137	. . . . . . . . . . 11 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏) ↔ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥))))
15	12, 14	anbi12d 477	. . . . . . . . . 10 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → ((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)) ↔ (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))))
16	15	imbi2d 230	. . . . . . . . 9 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → ((𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))) ↔ (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥))))))
17	16	rexralbidv 2576	. . . . . . . 8 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))) ↔ ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥))))))
18		simplrr 542	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) → ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))
19	18	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))
20		srpospr 8140	. . . . . . . . . 10 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)
21		riotacl 6044	. . . . . . . . . 10 ⊢ (∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥 → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
22	20, 21	syl 14	. . . . . . . . 9 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
23	22	adantll 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
24	17, 19, 23	rspcdva 2934	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))))
25		nfv 1581	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
26		nfv 1581	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑎 ∈ P
27		nfcv 2392	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗P
28		nfre1 2593	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
29	27, 28	nfralya 2590	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
30	26, 29	nfan 1618	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))
31	25, 30	nfan 1618	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))))
32		nfv 1581	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ R
33	31, 32	nfan 1618	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R)
34		nfv 1581	. . . . . . . . 9 ⊢ Ⅎ𝑗0_R <_R 𝑥
35	33, 34	nfan 1618	. . . . . . . 8 ⊢ Ⅎ𝑗(((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥)
36		nfv 1581	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝜑
37		nfv 1581	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑎 ∈ P
38		nfcv 2392	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘P
39		nfcv 2392	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘N
40		nfra1 2581	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
41	39, 40	nfrexya 2591	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
42	38, 41	nfralya 2590	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
43	37, 42	nfan 1618	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))
44	36, 43	nfan 1618	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))))
45		nfv 1581	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ R
46	44, 45	nfan 1618	. . . . . . . . . 10 ⊢ Ⅎ𝑘((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R)
47		nfv 1581	. . . . . . . . . 10 ⊢ Ⅎ𝑘0_R <_R 𝑥
48	46, 47	nfan 1618	. . . . . . . . 9 ⊢ Ⅎ𝑘(((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥)
49	5	ad4antr 498	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
50		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → 𝑘 ∈ N)
51	49, 50	ffvelcdmd 5835	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) ∈ P)
52		simplrl 541	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) → 𝑎 ∈ P)
53	52	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → 𝑎 ∈ P)
54		addclpr 7894	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
55	53, 23, 54	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
56	55	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
57		prsrlt 8144	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) ∈ P ∧ (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R <_R [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ))
58	51, 56, 57	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R <_R [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ))
59	1, 2, 3, 4	caucvgsrlemfv 8148	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
60	59	adantlr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
61	60	adantlr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
62	61	adantlr 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
63		prsradd 8143	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ))
64	53, 23, 63	syl2anc 415	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ))
65		prsrriota 8145	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
66	65	oveq2d 6091	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
67	66	adantll 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
68	64, 67	eqtrd 2271	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
69	68	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
70	62, 69	breq12d 4138	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R <_R [⟨((𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ↔ (𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
71	58, 70	bitrd 188	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ (𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
72	53	adantr 276	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → 𝑎 ∈ P)
73	23	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
74		addclpr 7894	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
75	51, 73, 74	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
76		prsrlt 8144	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ P ∧ (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P) → (𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R [⟨((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ))
77	72, 75, 76	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R [⟨((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ))
78		prsradd 8143	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → [⟨((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ))
79	51, 73, 78	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → [⟨((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R = ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ))
80	79	breq2d 4137	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R [⟨((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) +_P 1_P), 1_P⟩] ~_R ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R )))
81	65	adantll 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
82	81	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
83	62, 82	oveq12d 6093	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ) = ((𝐹‘𝑘) +_R 𝑥))
84	83	breq2d 4137	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ([⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R +_R [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R ) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)))
85	77, 80, 84	3bitrd 214	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → (𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)))
86	71, 85	anbi12d 477	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ((((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥))) ↔ ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥))))
87	86	imbi2d 230	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) ∧ 𝑘 ∈ N) → ((𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))) ↔ (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)))))
88	48, 87	ralbida 2544	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → (∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))) ↔ ∀𝑘 ∈ N (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)))))
89	35, 88	rexbid 2549	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → (∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))) ↔ ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)))))
90	24, 89	mpbid 147	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥))))
91		breq2 4129	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (𝑗 <_N 𝑘 ↔ 𝑗 <_N 𝑖))
92		fveq2 5690	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
93	92	breq1d 4135	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
94	92	oveq1d 6090	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +_R 𝑥) = ((𝐹‘𝑖) +_R 𝑥))
95	94	breq2d 4137	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
96	93, 95	anbi12d 477	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥)) ↔ ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))
97	91, 96	imbi12d 234	. . . . . . . 8 ⊢ (𝑘 = 𝑖 → ((𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥))) ↔ (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))))
98	97	cbvralv 2786	. . . . . . 7 ⊢ (∀𝑘 ∈ N (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥))) ↔ ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))
99	98	rexbii 2557	. . . . . 6 ⊢ (∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥))) ↔ ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))
100	90, 99	sylib 122	. . . . 5 ⊢ ((((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) ∧ 0_R <_R 𝑥) → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))
101	100	ex 115	. . . 4 ⊢ (((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) ∧ 𝑥 ∈ R) → (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))))
102	101	ralrimiva 2623	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) → ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))))
103		oveq1 6082	. . . . . . . . . 10 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 +_R 𝑥) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
104	103	breq2d 4137	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
105		breq1 4128	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 <_R ((𝐹‘𝑖) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
106	104, 105	anbi12d 477	. . . . . . . 8 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)) ↔ ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))
107	106	imbi2d 230	. . . . . . 7 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥))) ↔ (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))))
108	107	rexralbidv 2576	. . . . . 6 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥))) ↔ ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))))
109	108	imbi2d 230	. . . . 5 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))) ↔ (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))))
110	109	ralbidv 2550	. . . 4 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))) ↔ ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))))
111	110	rspcev 2929	. . 3 ⊢ (([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R ∧ ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ∧ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥))))) → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))
112	10, 102, 111	syl2anc 415	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ P ∧ ∀𝑏 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏))))) → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))
113	8, 112	rexlimddv 2673	1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1402 ∈ wcel 2209 {cab 2224 ∀wral 2528 ∃wrex 2529 ∃!wreu 2530 ⟨cop 3708 class class class wbr 4125 ↦ cmpt 4187 ⟶wf 5368 ‘cfv 5372 ℩crio 6027 (class class class)co 6075 1_oc1o 6670 [cec 6795 Ncnpi 7629 <_N clti 7632 ~_Q ceq 7636 *_Qcrq 7641 <_Q cltq 7642 Pcnp 7648 1_Pc1p 7649 +_P cpp 7650 <_P cltp 7652 ~_R cer 7653 Rcnr 7654 0_Rc0r 7655 1_Rc1r 7656 +_R cplr 7658 <_R cltr 7660

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 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 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730

This theorem 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-rmo 2536 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 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-eprel 4429 df-id 4433 df-po 4436 df-iso 4437 df-iord 4506 df-on 4508 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-irdg 6631 df-1o 6677 df-2o 6678 df-oadd 6681 df-omul 6682 df-er 6797 df-ec 6799 df-qs 6803 df-ni 7661 df-pli 7662 df-mi 7663 df-lti 7664 df-plpq 7701 df-mpq 7702 df-enq 7704 df-nqqs 7705 df-plqqs 7706 df-mqqs 7707 df-1nqqs 7708 df-rq 7709 df-ltnqqs 7710 df-enq0 7781 df-nq0 7782 df-0nq0 7783 df-plq0 7784 df-mq0 7785 df-inp 7823 df-i1p 7824 df-iplp 7825 df-iltp 7827 df-enr 8083 df-nr 8084 df-plr 8085 df-ltr 8087 df-0r 8088 df-1r 8089

This theorem is referenced by: caucvgsrlemoffres 8157

W3C validator