Theorem suplocsrlem 7770

Description: Lemma for suplocsr 7771. The set 𝐴 has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)

Hypotheses

Ref	Expression
suplocsrlem.b	⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}
suplocsrlem.ss	⊢ (𝜑 → 𝐴 ⊆ R)
suplocsrlem.c	⊢ (𝜑 → 𝐶 ∈ 𝐴)
suplocsrlem.ub	⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)
suplocsrlem.loc	⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))

Assertion

Ref	Expression
suplocsrlem	⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))

Distinct variable groups:   𝑤,𝐴,𝑥,𝑦,𝑧   𝑤,𝐵,𝑦,𝑧,𝑥   𝑤,𝐶,𝑦,𝑧,𝑥   𝜑,𝑤,𝑦,𝑥,𝑧

Proof of Theorem suplocsrlem

Dummy variables 𝑏 𝑢 𝑣 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suplocsrlem.b	. . 3 ⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}
2		suplocsrlem.ss	. . 3 ⊢ (𝜑 → 𝐴 ⊆ R)
3		suplocsrlem.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
4		suplocsrlem.ub	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)
5		suplocsrlem.loc	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))
6	1, 2, 3, 4, 5	suplocsrlempr 7769	. 2 ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
7		simpr 109	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝑣 ∈ P)
8	2, 3	sseldd 3148	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ R)
9	8	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝐶 ∈ R)
10		mappsrprg 7766	. . . . . . 7 ⊢ ((𝑣 ∈ P ∧ 𝐶 ∈ R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
11	7, 9, 10	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
12		ltrelsr 7700	. . . . . . 7 ⊢ <R ⊆ (R × R)
13	12	brel 4663	. . . . . 6 ⊢ ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
14	11, 13	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
15	14	simprd 113	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
16		breq2 3993	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑣<P 𝑤 ↔ 𝑣<P 𝑎))
17	16	notbid 662	. . . . . . 7 ⊢ (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
18	17	cbvralv 2696	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
19		ltsosr 7726	. . . . . . . . . . . . . . 15 ⊢ <R Or R
20	19, 12	sotri 5006	. . . . . . . . . . . . . 14 ⊢ (((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
21	11, 20	sylan 281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
22	9	adantr 274	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → 𝐶 ∈ R)
23		map2psrprg 7767	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ R → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
24	22, 23	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
25	21, 24	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
26	25	adantlr 474	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
27	26	adantlr 474	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
28		simplr 525	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
29		simprr 527	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
30	28, 29	breqtrrd 4017	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ))
31	7	ad4antr 491	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣 ∈ P)
32		simprl 526	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤 ∈ P)
33	9	ad4antr 491	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝐶 ∈ R)
34		ltpsrprg 7765	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ P ∧ 𝑤 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
35	31, 32, 33, 34	syl3anc 1233	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
36	30, 35	mpbid 146	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣<P 𝑤)
37		equcom 1699	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑎 ↔ 𝑎 = 𝑤)
38		bicom 139	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎) ↔ (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
39	17, 37, 38	3imtr3i 199	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
40		simp-4r 537	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
41		simpllr 529	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑦 ∈ 𝐴)
42	29, 41	eqeltrd 2247	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
43	1	rabeq2i 2727	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴))
44	32, 42, 43	sylanbrc 415	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤 ∈ 𝐵)
45	39, 40, 44	rspcdva 2839	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
46	36, 45	pm2.21fal 1368	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
47	27, 46	rexlimddv 2592	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
48	47	inegd 1367	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
49	48	ralrimiva 2543	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
50	49	ex 114	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
51	18, 50	syl5bi 151	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
52		nfv 1521	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑣 ∈ P)
53		nfra1 2501	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
54	52, 53	nfan 1558	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
55		nfv 1521	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ R
56	54, 55	nfan 1558	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R)
57		nfv 1521	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
58	56, 57	nfan 1558	. . . . . . . . . . 11 ⊢ Ⅎ𝑤((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59		nfv 1521	. . . . . . . . . . 11 ⊢ Ⅎ𝑤(𝐶 +R -1R) <R 𝑦
60	58, 59	nfan 1558	. . . . . . . . . 10 ⊢ Ⅎ𝑤(((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦)
61		simp-6r 541	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
62		simplr 525	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑤 ∈ P)
63		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
64		simp-4r 537	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
65	63, 64	eqbrtrd 4011	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
66		simp-7r 543	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑣 ∈ P)
67	9	ad4antr 491	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → 𝐶 ∈ R)
68	67	ad2antrr 485	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝐶 ∈ R)
69		ltpsrprg 7765	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
70	62, 66, 68, 69	syl3anc 1233	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
71	65, 70	mpbid 146	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑤<P 𝑣)
72		rsp 2517	. . . . . . . . . . . . 13 ⊢ (∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → (𝑤 ∈ P → (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
73	61, 62, 71, 72	syl3c 63	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
74		breq2 3993	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑏 → (𝑤<P 𝑢 ↔ 𝑤<P 𝑏))
75	74	cbvrexv 2697	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝐵 𝑤<P 𝑢 ↔ ∃𝑏 ∈ 𝐵 𝑤<P 𝑏)
76	73, 75	sylib 121	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑏 ∈ 𝐵 𝑤<P 𝑏)
77		simprl 526	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑏 ∈ 𝐵)
78		opeq1 3765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
79	78	eceq1d 6549	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
80	79	oveq2d 5869	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
81	80	eleq1d 2239	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
82	81, 1	elrab2 2889	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ P ∧ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
83	77, 82	sylib 121	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝑏 ∈ P ∧ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
84	83	simprd 113	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴)
85		simplr 525	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
86		simprr 527	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑤<P 𝑏)
87		simpllr 529	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑤 ∈ P)
88	83	simpld 111	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑏 ∈ P)
89	67	ad3antrrr 489	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝐶 ∈ R)
90		ltpsrprg 7765	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑏 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
91	87, 88, 89, 90	syl3anc 1233	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
92	86, 91	mpbird 166	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
93	85, 92	eqbrtrrd 4013	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94		breq2 3993	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧 ↔ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
95	94	rspcev 2834	. . . . . . . . . . . 12 ⊢ (((𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴 ∧ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
96	84, 93, 95	syl2anc 409	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
97	76, 96	rexlimddv 2592	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
98		simpr 109	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
99	67, 23	syl 14	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
100	98, 99	mpbid 146	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
101	60, 97, 100	r19.29af 2611	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
102	3	ad5antr 493	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → 𝐶 ∈ 𝐴)
103		breq2 3993	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶))
104	103	rspcev 2834	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
105	102, 104	sylancom 418	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
106		ltm1sr 7739	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ R → (𝐶 +R -1R) <R 𝐶)
107	8, 106	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 +R -1R) <R 𝐶)
108	107	ad4antr 491	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) <R 𝐶)
109	9	ad3antrrr 489	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝐶 ∈ R)
110		m1r 7714	. . . . . . . . . . . 12 ⊢ -1R ∈ R
111		addclsr 7715	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 +R -1R) ∈ R)
112	109, 110, 111	sylancl 411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) ∈ R)
113		simplr 525	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝑦 ∈ R)
114		sowlin 4305	. . . . . . . . . . . 12 ⊢ (( <R Or R ∧ ((𝐶 +R -1R) ∈ R ∧ 𝐶 ∈ R ∧ 𝑦 ∈ R)) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶)))
115	19, 114	mpan 422	. . . . . . . . . . 11 ⊢ (((𝐶 +R -1R) ∈ R ∧ 𝐶 ∈ R ∧ 𝑦 ∈ R) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶)))
116	112, 109, 113, 115	syl3anc 1233	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶)))
117	108, 116	mpd 13	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶))
118	101, 105, 117	mpjaodan 793	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
119	118	ex 114	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))
120	119	ralrimiva 2543	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))
121	120	ex 114	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
122	51, 121	anim12d 333	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
123		breq1 3992	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
124	123	notbid 662	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
125	124	ralbidv 2470	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126		breq2 3993	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑦 <R 𝑥 ↔ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
127	126	imbi1d 230	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
128	127	ralbidv 2470	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
129	125, 128	anbi12d 470	. . . . 5 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
130	129	rspcev 2834	. . . 4 ⊢ (((𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R ∧ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
131	15, 122, 130	syl6an 1427	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
132	131	rexlimdva 2587	. 2 ⊢ (𝜑 → (∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
133	6, 132	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 703   ∧ w3a 973   = wceq 1348  ⊥wfal 1353   ∈ wcel 2141  ∀wral 2448  ∃wrex 2449  {crab 2452   ⊆ wss 3121  ⟨cop 3586   class class class wbr 3989   Or wor 4280  (class class class)co 5853  [cec 6511  Pcnp 7253  1_Pc1p 7254  <_P cltp 7257   ~_R cer 7258  Rcnr 7259  -1_Rcm1r 7262   +_R cplr 7263   <_R cltr 7265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-eprel 4274  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-1o 6395  df-2o 6396  df-oadd 6399  df-omul 6400  df-er 6513  df-ec 6515  df-qs 6519  df-ni 7266  df-pli 7267  df-mi 7268  df-lti 7269  df-plpq 7306  df-mpq 7307  df-enq 7309  df-nqqs 7310  df-plqqs 7311  df-mqqs 7312  df-1nqqs 7313  df-rq 7314  df-ltnqqs 7315  df-enq0 7386  df-nq0 7387  df-0nq0 7388  df-plq0 7389  df-mq0 7390  df-inp 7428  df-i1p 7429  df-iplp 7430  df-imp 7431  df-iltp 7432  df-enr 7688  df-nr 7689  df-plr 7690  df-mr 7691  df-ltr 7692  df-0r 7693  df-1r 7694  df-m1r 7695

This theorem is referenced by:  suplocsr  7771