caucvgsrlemgt1 - Intuitionistic Logic Explorer

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

Theorem caucvgsrlemgt1 6879

Description: Lemma for caucvgsr 6886. 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_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ) ∧ (𝐹‘𝑘) <_R ((𝐹‘𝑛) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_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_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ) ∧ (𝐹‘𝑘) <_R ((𝐹‘𝑛) +_R [⟨(⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩ +_P 1_P), 1_P⟩] ~_R ))))
3		caucvgsrlemgt1.gt1	. . . 4 ⊢ (𝜑 → ∀𝑚 ∈ N 1_R <_R (𝐹‘𝑚))
4		eqid 2040	. . . 4 ⊢ (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )) = (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))
5	1, 2, 3, 4	caucvgsrlemf 6876	. . 3 ⊢ (𝜑 → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
6	1, 2, 3, 4	caucvgsrlemcau 6877	. . 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_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩) ∧ ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑛) +_P ⟨{𝑙 ∣ 𝑙 <_Q (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q )}, {𝑢 ∣ (_Q‘[⟨𝑛, 1_𝑜⟩] ~_Q ) <_Q 𝑢}⟩))))
7	1, 2, 3, 4	caucvgsrlembound 6878	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ N 1_P<_P ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑚))
8	5, 6, 7	caucvgprpr 6810	. 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 6868	. . . 4 ⊢ (𝑎 ∈ P → [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R)
10	9	ad2antrl 459	. . 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		srpospr 6867	. . . . . . . . . 10 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)
12		riotacl 5482	. . . . . . . . . 10 ⊢ (∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥 → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
13	11, 12	syl 14	. . . . . . . . 9 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P)
14	13	adantll 445	. . . . . . . 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)
15		simplrr 488	. . . . . . . . 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 𝑏))))
16	15	adantr 261	. . . . . . . 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 𝑏))))
17		oveq2 5520	. . . . . . . . . . . . 13 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎 +_P 𝑏) = (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
18	17	breq2d 3776	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥))))
19		oveq2 5520	. . . . . . . . . . . . 13 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥)))
20	19	breq2d 3776	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥))))
21	18, 20	anbi12d 442	. . . . . . . . . . 11 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥)))))
22	21	imbi2d 219	. . . . . . . . . 10 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥))))))
23	22	rexralbidv 2350	. . . . . . . . 9 ⊢ (𝑏 = (℩𝑐 ∈ 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 = 𝑥))))))
24	23	rspcva 2654	. . . . . . . 8 ⊢ (((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ 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 (𝑗 <_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	14, 16, 24	syl2anc 391	. . . . . . 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 = 𝑥)))))
26		nfv 1421	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
27		nfv 1421	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑎 ∈ P
28		nfcv 2178	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗P
29		nfre1 2365	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
30	28, 29	nfralya 2362	. . . . . . . . . . . 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 𝑏)))
31	27, 30	nfan 1457	. . . . . . . . . . 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 𝑏))))
32	26, 31	nfan 1457	. . . . . . . . . 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 𝑏)))))
33		nfv 1421	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ R
34	32, 33	nfan 1457	. . . . . . . . 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)
35		nfv 1421	. . . . . . . . 9 ⊢ Ⅎ𝑗0_R <_R 𝑥
36	34, 35	nfan 1457	. . . . . . . 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 𝑥)
37		nfv 1421	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝜑
38		nfv 1421	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑎 ∈ P
39		nfcv 2178	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘P
40		nfcv 2178	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘N
41		nfra1 2355	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
42	40, 41	nfrexya 2363	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <_N 𝑘 → (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘)<_P (𝑎 +_P 𝑏) ∧ 𝑎<_P (((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 𝑏)))
43	39, 42	nfralya 2362	. . . . . . . . . . . . 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 𝑏)))
44	38, 43	nfan 1457	. . . . . . . . . . . 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 𝑏))))
45	37, 44	nfan 1457	. . . . . . . . . . 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 𝑏)))))
46		nfv 1421	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ R
47	45, 46	nfan 1457	. . . . . . . . . 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)
48		nfv 1421	. . . . . . . . . 10 ⊢ Ⅎ𝑘0_R <_R 𝑥
49	47, 48	nfan 1457	. . . . . . . . 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 𝑥)
50	5	ad4antr 463	. . . . . . . . . . . . . 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)
51		simpr 103	. . . . . . . . . . . . . 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)
52	50, 51	ffvelrnd 5303	. . . . . . . . . . . . 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)
53		simplrl 487	. . . . . . . . . . . . . . . 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)
54	53	adantr 261	. . . . . . . . . . . . . . 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)
55		addclpr 6635	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
56	54, 14, 55	syl2anc 391	. . . . . . . . . . . . . 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)
57	56	adantr 261	. . . . . . . . . . . . 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)
58		prsrlt 6871	. . . . . . . . . . . . 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 ))
59	52, 57, 58	syl2anc 391	. . . . . . . . . . . 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 ))
60	1, 2, 3, 4	caucvgsrlemfv 6875	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
61	60	adantlr 446	. . . . . . . . . . . . . . 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 = (𝐹‘𝑘))
62	61	adantlr 446	. . . . . . . . . . . . . 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 = (𝐹‘𝑘))
63	62	adantlr 446	. . . . . . . . . . . . 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 = (𝐹‘𝑘))
64		prsradd 6870	. . . . . . . . . . . . . . . 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 ))
65	54, 14, 64	syl2anc 391	. . . . . . . . . . . . . . 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 ))
66		prsrriota 6872	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
67	66	oveq2d 5528	. . . . . . . . . . . . . . . 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 𝑥))
68	67	adantll 445	. . . . . . . . . . . . . . 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 𝑥))
69	65, 68	eqtrd 2072	. . . . . . . . . . . . . 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 𝑥))
70	69	adantr 261	. . . . . . . . . . . . 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 𝑥))
71	63, 70	breq12d 3777	. . . . . . . . . . . 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 𝑥)))
72	59, 71	bitrd 177	. . . . . . . . . . 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 𝑥)))
73	54	adantr 261	. . . . . . . . . . . . 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)
74	14	adantr 261	. . . . . . . . . . . . . 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)
75		addclpr 6635	. . . . . . . . . . . . . 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)
76	52, 74, 75	syl2anc 391	. . . . . . . . . . . . 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)
77		prsrlt 6871	. . . . . . . . . . . . 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 ))
78	73, 76, 77	syl2anc 391	. . . . . . . . . . . 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 ))
79		prsradd 6870	. . . . . . . . . . . . . 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 ))
80	52, 74, 79	syl2anc 391	. . . . . . . . . . . . 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 ))
81	80	breq2d 3776	. . . . . . . . . . . 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 )))
82	66	adantll 445	. . . . . . . . . . . . . . 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 = 𝑥)
83	82	adantr 261	. . . . . . . . . . . . . 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 = 𝑥)
84	63, 83	oveq12d 5530	. . . . . . . . . . . . 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 𝑥))
85	84	breq2d 3776	. . . . . . . . . . . 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 𝑥)))
86	78, 81, 85	3bitrd 203	. . . . . . . . . . 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 𝑥)))
87	72, 86	anbi12d 442	. . . . . . . . . 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 𝑥))))
88	87	imbi2d 219	. . . . . . . . 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 𝑥)))))
89	49, 88	ralbida 2320	. . . . . . . 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 𝑥)))))
90	36, 89	rexbid 2325	. . . . . . 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 𝑥)))))
91	25, 90	mpbid 135	. . . . . 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 𝑥))))
92		breq2 3768	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (𝑗 <_N 𝑘 ↔ 𝑗 <_N 𝑖))
93		fveq2 5178	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
94	93	breq1d 3774	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
95	93	oveq1d 5527	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +_R 𝑥) = ((𝐹‘𝑖) +_R 𝑥))
96	95	breq2d 3776	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
97	94, 96	anbi12d 442	. . . . . . . . 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 𝑥))))
98	92, 97	imbi12d 223	. . . . . . . 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 𝑥)))))
99	98	cbvralv 2533	. . . . . . 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 𝑥))))
100	99	rexbii 2331	. . . . . 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 𝑥))))
101	91, 100	sylib 127	. . . . 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 𝑥))))
102	101	ex 108	. . . 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 𝑥)))))
103	102	ralrimiva 2392	. . 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 𝑥)))))
104		oveq1 5519	. . . . . . . . . 10 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 +_R 𝑥) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
105	104	breq2d 3776	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
106		breq1 3767	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 <_R ((𝐹‘𝑖) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
107	105, 106	anbi12d 442	. . . . . . . 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 𝑥))))
108	107	imbi2d 219	. . . . . . 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 𝑥)))))
109	108	rexralbidv 2350	. . . . . 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 𝑥)))))
110	109	imbi2d 219	. . . . 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 𝑥))))))
111	110	ralbidv 2326	. . . 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 𝑥))))))
112	111	rspcev 2656	. . 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 𝑥)))))
113	10, 103, 112	syl2anc 391	. 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 𝑥)))))
114	8, 113	rexlimddv 2437	1 ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0_R <_R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <_N 𝑖 → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ∧ 𝑦 <_R ((𝐹‘𝑖) +_R 𝑥)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 = wceq 1243 ∈ wcel 1393 {cab 2026 ∀wral 2306 ∃wrex 2307 ∃!wreu 2308 ⟨cop 3378 class class class wbr 3764 ↦ cmpt 3818 ⟶wf 4898 ‘cfv 4902 ℩crio 5467 (class class class)co 5512 1_𝑜c1o 5994 [cec 6104 Ncnpi 6370 <_N clti 6373 ~_Q ceq 6377 *_Qcrq 6382 <_Q cltq 6383 Pcnp 6389 1_Pc1p 6390 +_P cpp 6391 <_P cltp 6393 ~_R cer 6394 Rcnr 6395 0_Rc0r 6396 1_Rc1r 6397 +_R cplr 6399 <_R cltr 6401

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-coll 3872 ax-sep 3875 ax-nul 3883 ax-pow 3927 ax-pr 3944 ax-un 4170 ax-setind 4262 ax-iinf 4311

This theorem depends on definitions: df-bi 110 df-dc 743 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-ral 2311 df-rex 2312 df-reu 2313 df-rmo 2314 df-rab 2315 df-v 2559 df-sbc 2765 df-csb 2853 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-nul 3225 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-iun 3659 df-br 3765 df-opab 3819 df-mpt 3820 df-tr 3855 df-eprel 4026 df-id 4030 df-po 4033 df-iso 4034 df-iord 4103 df-on 4105 df-suc 4108 df-iom 4314 df-xp 4351 df-rel 4352 df-cnv 4353 df-co 4354 df-dm 4355 df-rn 4356 df-res 4357 df-ima 4358 df-iota 4867 df-fun 4904 df-fn 4905 df-f 4906 df-f1 4907 df-fo 4908 df-f1o 4909 df-fv 4910 df-riota 5468 df-ov 5515 df-oprab 5516 df-mpt2 5517 df-1st 5767 df-2nd 5768 df-recs 5920 df-irdg 5957 df-1o 6001 df-2o 6002 df-oadd 6005 df-omul 6006 df-er 6106 df-ec 6108 df-qs 6112 df-ni 6402 df-pli 6403 df-mi 6404 df-lti 6405 df-plpq 6442 df-mpq 6443 df-enq 6445 df-nqqs 6446 df-plqqs 6447 df-mqqs 6448 df-1nqqs 6449 df-rq 6450 df-ltnqqs 6451 df-enq0 6522 df-nq0 6523 df-0nq0 6524 df-plq0 6525 df-mq0 6526 df-inp 6564 df-i1p 6565 df-iplp 6566 df-iltp 6568 df-enr 6811 df-nr 6812 df-plr 6813 df-ltr 6815 df-0r 6816 df-1r 6817

This theorem is referenced by: caucvgsrlemoffres 6884

W3C validator