caucvgsrlemgt1 - Intuitionistic Logic Explorer

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

Theorem caucvgsrlemgt1 7736

Description: Lemma for caucvgsr 7743. 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 2165	. . . 4 ⊢ (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )) = (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))
5	1, 2, 3, 4	caucvgsrlemf 7733	. . 3 ⊢ (𝜑 → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
6	1, 2, 3, 4	caucvgsrlemcau 7734	. . 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 7735	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ N 1_P<_P ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑚))
8	5, 6, 7	caucvgprpr 7653	. 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 7725	. . . 4 ⊢ (𝑎 ∈ P → [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R)
10	9	ad2antrl 482	. . 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 5850	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎 +_P 𝑏) = (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
12	11	breq2d 3994	. . . . . . . . . . 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 5850	. . . . . . . . . . . 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 3994	. . . . . . . . . . 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 465	. . . . . . . . . 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 229	. . . . . . . . 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 2492	. . . . . . . 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 526	. . . . . . . . 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 274	. . . . . . . 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 7724	. . . . . . . . . 10 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)
21		riotacl 5812	. . . . . . . . . 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 468	. . . . . . . 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 2835	. . . . . . 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 1516	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
26		nfv 1516	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑎 ∈ P
27		nfcv 2308	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗P
28		nfre1 2509	. . . . . . . . . . . . 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 2506	. . . . . . . . . . . 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 1553	. . . . . . . . . . 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 1553	. . . . . . . . . 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 1516	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ R
33	31, 32	nfan 1553	. . . . . . . . 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 1516	. . . . . . . . 9 ⊢ Ⅎ𝑗0_R <_R 𝑥
35	33, 34	nfan 1553	. . . . . . . 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 1516	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝜑
37		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑎 ∈ P
38		nfcv 2308	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘P
39		nfcv 2308	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘N
40		nfra1 2497	. . . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . . 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 2506	. . . . . . . . . . . . 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 1553	. . . . . . . . . . . 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 1553	. . . . . . . . . . 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 1516	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ R
46	44, 45	nfan 1553	. . . . . . . . . 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 1516	. . . . . . . . . 10 ⊢ Ⅎ𝑘0_R <_R 𝑥
48	46, 47	nfan 1553	. . . . . . . . 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 486	. . . . . . . . . . . . . 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 109	. . . . . . . . . . . . . 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	ffvelrnd 5621	. . . . . . . . . . . . 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 525	. . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . 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 7478	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
55	53, 23, 54	syl2anc 409	. . . . . . . . . . . . . 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 274	. . . . . . . . . . . . 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 7728	. . . . . . . . . . . . 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 409	. . . . . . . . . . . 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 7732	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
60	59	adantlr 469	. . . . . . . . . . . . . . 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 469	. . . . . . . . . . . . . 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 469	. . . . . . . . . . . . 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 7727	. . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . 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 7729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
66	65	oveq2d 5858	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 2198	. . . . . . . . . . . . . 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 274	. . . . . . . . . . . . 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 3995	. . . . . . . . . . . 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 187	. . . . . . . . . . 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 274	. . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 7478	. . . . . . . . . . . . . 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 409	. . . . . . . . . . . . 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 7728	. . . . . . . . . . . . 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 409	. . . . . . . . . . . 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 7727	. . . . . . . . . . . . . 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 409	. . . . . . . . . . . . 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 3994	. . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 5860	. . . . . . . . . . . . 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 3994	. . . . . . . . . . . 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 213	. . . . . . . . . . 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 465	. . . . . . . . . 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 229	. . . . . . . . 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 2460	. . . . . . . 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 2465	. . . . . . 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 146	. . . . . 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 3986	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (𝑗 <_N 𝑘 ↔ 𝑗 <_N 𝑖))
92		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
93	92	breq1d 3992	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
94	92	oveq1d 5857	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +_R 𝑥) = ((𝐹‘𝑖) +_R 𝑥))
95	94	breq2d 3994	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
96	93, 95	anbi12d 465	. . . . . . . . 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 233	. . . . . . . 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 2692	. . . . . . 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 2473	. . . . . 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 121	. . . . 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 114	. . . 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 2539	. . 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 5849	. . . . . . . . . 10 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 +_R 𝑥) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
104	103	breq2d 3994	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
105		breq1 3985	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 <_R ((𝐹‘𝑖) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
106	104, 105	anbi12d 465	. . . . . . . 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 229	. . . . . . 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 2492	. . . . . 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 229	. . . . 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 2466	. . . 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 2830	. . 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 409	. 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 2588	1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1343 ∈ wcel 2136 {cab 2151 ∀wral 2444 ∃wrex 2445 ∃!wreu 2446 ⟨cop 3579 class class class wbr 3982 ↦ cmpt 4043 ⟶wf 5184 ‘cfv 5188 ℩crio 5797 (class class class)co 5842 1_oc1o 6377 [cec 6499 Ncnpi 7213 <_N clti 7216 ~_Q ceq 7220 *_Qcrq 7225 <_Q cltq 7226 Pcnp 7232 1_Pc1p 7233 +_P cpp 7234 <_P cltp 7236 ~_R cer 7237 Rcnr 7238 0_Rc0r 7239 1_Rc1r 7240 +_R cplr 7242 <_R cltr 7244

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-eprel 4267 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-1o 6384 df-2o 6385 df-oadd 6388 df-omul 6389 df-er 6501 df-ec 6503 df-qs 6507 df-ni 7245 df-pli 7246 df-mi 7247 df-lti 7248 df-plpq 7285 df-mpq 7286 df-enq 7288 df-nqqs 7289 df-plqqs 7290 df-mqqs 7291 df-1nqqs 7292 df-rq 7293 df-ltnqqs 7294 df-enq0 7365 df-nq0 7366 df-0nq0 7367 df-plq0 7368 df-mq0 7369 df-inp 7407 df-i1p 7408 df-iplp 7409 df-iltp 7411 df-enr 7667 df-nr 7668 df-plr 7669 df-ltr 7671 df-0r 7672 df-1r 7673

This theorem is referenced by: caucvgsrlemoffres 7741

W3C validator