caucvgsrlemgt1 - Intuitionistic Logic Explorer

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

Theorem caucvgsrlemgt1 7908

Description: Lemma for caucvgsr 7915. 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 2205	. . . 4 ⊢ (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )) = (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))
5	1, 2, 3, 4	caucvgsrlemf 7905	. . 3 ⊢ (𝜑 → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
6	1, 2, 3, 4	caucvgsrlemcau 7906	. . 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 7907	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ N 1_P<_P ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑚))
8	5, 6, 7	caucvgprpr 7825	. 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 7897	. . . 4 ⊢ (𝑎 ∈ P → [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R ∈ R)
10	9	ad2antrl 490	. . 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 5952	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎 +_P 𝑏) = (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
12	11	breq2d 4056	. . . . . . . . . . 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 5952	. . . . . . . . . . . 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 4056	. . . . . . . . . . 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 473	. . . . . . . . . 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 2532	. . . . . . . 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 536	. . . . . . . . 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 7896	. . . . . . . . . 10 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)
21		riotacl 5914	. . . . . . . . . 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 476	. . . . . . . 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 2882	. . . . . . 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 1551	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
26		nfv 1551	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑎 ∈ P
27		nfcv 2348	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗P
28		nfre1 2549	. . . . . . . . . . . . 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 2546	. . . . . . . . . . . 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 1588	. . . . . . . . . . 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 1588	. . . . . . . . . 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 1551	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ R
33	31, 32	nfan 1588	. . . . . . . . 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 1551	. . . . . . . . 9 ⊢ Ⅎ𝑗0_R <_R 𝑥
35	33, 34	nfan 1588	. . . . . . . 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 1551	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝜑
37		nfv 1551	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑎 ∈ P
38		nfcv 2348	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘P
39		nfcv 2348	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘N
40		nfra1 2537	. . . . . . . . . . . . . . 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 2547	. . . . . . . . . . . . . 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 2546	. . . . . . . . . . . . 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 1588	. . . . . . . . . . . 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 1588	. . . . . . . . . . 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 1551	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ R
46	44, 45	nfan 1588	. . . . . . . . . 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 1551	. . . . . . . . . 10 ⊢ Ⅎ𝑘0_R <_R 𝑥
48	46, 47	nfan 1588	. . . . . . . . 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 494	. . . . . . . . . . . . . 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 5716	. . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . . 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 7650	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ P ∧ (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) ∈ P) → (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)) ∈ P)
55	53, 23, 54	syl2anc 411	. . . . . . . . . . . . . 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 7900	. . . . . . . . . . . . 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 411	. . . . . . . . . . . 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 7904	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ N) → [⟨(((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑘) +_P 1_P), 1_P⟩] ~_R = (𝐹‘𝑘))
60	59	adantlr 477	. . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . 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 477	. . . . . . . . . . . . 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 7899	. . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . 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 7901	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
66	65	oveq2d 5960	. . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . 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 2238	. . . . . . . . . . . . . 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 4057	. . . . . . . . . . . 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 7650	. . . . . . . . . . . . . 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 411	. . . . . . . . . . . . 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 7900	. . . . . . . . . . . . 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 411	. . . . . . . . . . . 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 7899	. . . . . . . . . . . . . 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 411	. . . . . . . . . . . . 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 4056	. . . . . . . . . . . 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 476	. . . . . . . . . . . . . . 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 5962	. . . . . . . . . . . . 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 4056	. . . . . . . . . . . 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 473	. . . . . . . . . 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 2500	. . . . . . . 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 2505	. . . . . . 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 4048	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (𝑗 <_N 𝑘 ↔ 𝑗 <_N 𝑖))
92		fveq2 5576	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
93	92	breq1d 4054	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
94	92	oveq1d 5959	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +_R 𝑥) = ((𝐹‘𝑖) +_R 𝑥))
95	94	breq2d 4056	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑘) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
96	93, 95	anbi12d 473	. . . . . . . . 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 2738	. . . . . . 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 2513	. . . . . 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 2579	. . 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 5951	. . . . . . . . . 10 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 +_R 𝑥) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
104	103	breq2d 4056	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
105		breq1 4047	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 <_R ((𝐹‘𝑖) +_R 𝑥) ↔ [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R <_R ((𝐹‘𝑖) +_R 𝑥)))
106	104, 105	anbi12d 473	. . . . . . . 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 2532	. . . . . 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 2506	. . . 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 2877	. . 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 411	. 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 2628	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 1373 ∈ wcel 2176 {cab 2191 ∀wral 2484 ∃wrex 2485 ∃!wreu 2486 ⟨cop 3636 class class class wbr 4044 ↦ cmpt 4105 ⟶wf 5267 ‘cfv 5271 ℩crio 5898 (class class class)co 5944 1_oc1o 6495 [cec 6618 Ncnpi 7385 <_N clti 7388 ~_Q ceq 7392 *_Qcrq 7397 <_Q cltq 7398 Pcnp 7404 1_Pc1p 7405 +_P cpp 7406 <_P cltp 7408 ~_R cer 7409 Rcnr 7410 0_Rc0r 7411 1_Rc1r 7412 +_R cplr 7414 <_R cltr 7416

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4159 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-iinf 4636

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4045 df-opab 4106 df-mpt 4107 df-tr 4143 df-eprel 4336 df-id 4340 df-po 4343 df-iso 4344 df-iord 4413 df-on 4415 df-suc 4418 df-iom 4639 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-f1 5276 df-fo 5277 df-f1o 5278 df-fv 5279 df-riota 5899 df-ov 5947 df-oprab 5948 df-mpo 5949 df-1st 6226 df-2nd 6227 df-recs 6391 df-irdg 6456 df-1o 6502 df-2o 6503 df-oadd 6506 df-omul 6507 df-er 6620 df-ec 6622 df-qs 6626 df-ni 7417 df-pli 7418 df-mi 7419 df-lti 7420 df-plpq 7457 df-mpq 7458 df-enq 7460 df-nqqs 7461 df-plqqs 7462 df-mqqs 7463 df-1nqqs 7464 df-rq 7465 df-ltnqqs 7466 df-enq0 7537 df-nq0 7538 df-0nq0 7539 df-plq0 7540 df-mq0 7541 df-inp 7579 df-i1p 7580 df-iplp 7581 df-iltp 7583 df-enr 7839 df-nr 7840 df-plr 7841 df-ltr 7843 df-0r 7844 df-1r 7845

This theorem is referenced by: caucvgsrlemoffres 7913

W3C validator