caucvgsrlemgt1 - Intuitionistic Logic Explorer

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

Theorem caucvgsrlemgt1 7978

Description: Lemma for caucvgsr 7985. 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 2229	. . . 4 ⊢ (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )) = (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))
5	1, 2, 3, 4	caucvgsrlemf 7975	. . 3 ⊢ (𝜑 → (𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R )):N⟶P)
6	1, 2, 3, 4	caucvgsrlemcau 7976	. . 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 7977	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ N 1_P<_P ((𝑧 ∈ N ↦ (℩𝑤 ∈ P (𝐹‘𝑧) = [⟨(𝑤 +_P 1_P), 1_P⟩] ~_R ))‘𝑚))
8	5, 6, 7	caucvgprpr 7895	. 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 7967	. . . 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 6008	. . . . . . . . . . . 12 ⊢ (𝑏 = (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) → (𝑎 +_P 𝑏) = (𝑎 +_P (℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)))
12	11	breq2d 4094	. . . . . . . . . . 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 6008	. . . . . . . . . . . 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 4094	. . . . . . . . . . 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 2556	. . . . . . . 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 7966	. . . . . . . . . 10 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → ∃!𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥)
21		riotacl 5969	. . . . . . . . . 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 2912	. . . . . . 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 1574	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
26		nfv 1574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑎 ∈ P
27		nfcv 2372	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗P
28		nfre1 2573	. . . . . . . . . . . . 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 2570	. . . . . . . . . . . 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 1611	. . . . . . . . . . 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 1611	. . . . . . . . . 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 1574	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ R
33	31, 32	nfan 1611	. . . . . . . . 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 1574	. . . . . . . . 9 ⊢ Ⅎ𝑗0_R <_R 𝑥
35	33, 34	nfan 1611	. . . . . . . 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 1574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝜑
37		nfv 1574	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑎 ∈ P
38		nfcv 2372	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘P
39		nfcv 2372	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘N
40		nfra1 2561	. . . . . . . . . . . . . . 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 2571	. . . . . . . . . . . . . 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 2570	. . . . . . . . . . . . 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 1611	. . . . . . . . . . . 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 1611	. . . . . . . . . . 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 1574	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑥 ∈ R
46	44, 45	nfan 1611	. . . . . . . . . 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 1574	. . . . . . . . . 10 ⊢ Ⅎ𝑘0_R <_R 𝑥
48	46, 47	nfan 1611	. . . . . . . . 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 5770	. . . . . . . . . . . . 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 7720	. . . . . . . . . . . . . . 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 7970	. . . . . . . . . . . . 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 7974	. . . . . . . . . . . . . . . 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 7969	. . . . . . . . . . . . . . . 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 7971	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ R ∧ 0_R <_R 𝑥) → [⟨((℩𝑐 ∈ P [⟨(𝑐 +_P 1_P), 1_P⟩] ~_R = 𝑥) +_P 1_P), 1_P⟩] ~_R = 𝑥)
66	65	oveq2d 6016	. . . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . . 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 4095	. . . . . . . . . . . 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 7720	. . . . . . . . . . . . . 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 7970	. . . . . . . . . . . . 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 7969	. . . . . . . . . . . . . 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 4094	. . . . . . . . . . . 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 6018	. . . . . . . . . . . . 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 4094	. . . . . . . . . . . 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 2524	. . . . . . . 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 2529	. . . . . . 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 4086	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (𝑗 <_N 𝑘 ↔ 𝑗 <_N 𝑖))
92		fveq2 5626	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖))
93	92	breq1d 4092	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
94	92	oveq1d 6015	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) +_R 𝑥) = ((𝐹‘𝑖) +_R 𝑥))
95	94	breq2d 4094	. . . . . . . . . 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 2765	. . . . . . 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 2537	. . . . . 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 2603	. . 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 6007	. . . . . . . . . 10 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → (𝑦 +_R 𝑥) = ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥))
104	103	breq2d 4094	. . . . . . . . 9 ⊢ (𝑦 = [⟨(𝑎 +_P 1_P), 1_P⟩] ~_R → ((𝐹‘𝑖) <_R (𝑦 +_R 𝑥) ↔ (𝐹‘𝑖) <_R ([⟨(𝑎 +_P 1_P), 1_P⟩] ~_R +_R 𝑥)))
105		breq1 4085	. . . . . . . . 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 2556	. . . . . 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 2530	. . . 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 2907	. . 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 2653	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 1395 ∈ wcel 2200 {cab 2215 ∀wral 2508 ∃wrex 2509 ∃!wreu 2510 ⟨cop 3669 class class class wbr 4082 ↦ cmpt 4144 ⟶wf 5313 ‘cfv 5317 ℩crio 5952 (class class class)co 6000 1_oc1o 6553 [cec 6676 Ncnpi 7455 <_N clti 7458 ~_Q ceq 7462 *_Qcrq 7467 <_Q cltq 7468 Pcnp 7474 1_Pc1p 7475 +_P cpp 7476 <_P cltp 7478 ~_R cer 7479 Rcnr 7480 0_Rc0r 7481 1_Rc1r 7482 +_R cplr 7484 <_R cltr 7486

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-eprel 4379 df-id 4383 df-po 4386 df-iso 4387 df-iord 4456 df-on 4458 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-irdg 6514 df-1o 6560 df-2o 6561 df-oadd 6564 df-omul 6565 df-er 6678 df-ec 6680 df-qs 6684 df-ni 7487 df-pli 7488 df-mi 7489 df-lti 7490 df-plpq 7527 df-mpq 7528 df-enq 7530 df-nqqs 7531 df-plqqs 7532 df-mqqs 7533 df-1nqqs 7534 df-rq 7535 df-ltnqqs 7536 df-enq0 7607 df-nq0 7608 df-0nq0 7609 df-plq0 7610 df-mq0 7611 df-inp 7649 df-i1p 7650 df-iplp 7651 df-iltp 7653 df-enr 7909 df-nr 7910 df-plr 7911 df-ltr 7913 df-0r 7914 df-1r 7915

This theorem is referenced by: caucvgsrlemoffres 7983

W3C validator