Theorem suplocsrlem 7991

Description: Lemma for suplocsr 7992. 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 7990	. 2 ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
7		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝑣 ∈ P)
8	2, 3	sseldd 3225	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ R)
9	8	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝐶 ∈ R)
10		mappsrprg 7987	. . . . . . 7 ⊢ ((𝑣 ∈ P ∧ 𝐶 ∈ R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
11	7, 9, 10	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
12		ltrelsr 7921	. . . . . . 7 ⊢ <R ⊆ (R × R)
13	12	brel 4770	. . . . . 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 114	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
16		breq2 4086	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑣<P 𝑤 ↔ 𝑣<P 𝑎))
17	16	notbid 671	. . . . . . 7 ⊢ (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
18	17	cbvralv 2765	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
19		ltsosr 7947	. . . . . . . . . . . . . . 15 ⊢ <R Or R
20	19, 12	sotri 5123	. . . . . . . . . . . . . 14 ⊢ (((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
21	11, 20	sylan 283	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
22	9	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → 𝐶 ∈ R)
23		map2psrprg 7988	. . . . . . . . . . . . . 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 147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
26	25	adantlr 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
27	26	adantlr 477	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
28		simplr 528	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
29		simprr 531	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
30	28, 29	breqtrrd 4110	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ))
31	7	ad4antr 494	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣 ∈ P)
32		simprl 529	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤 ∈ P)
33	9	ad4antr 494	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝐶 ∈ R)
34		ltpsrprg 7986	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ P ∧ 𝑤 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
35	31, 32, 33, 34	syl3anc 1271	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
36	30, 35	mpbid 147	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣<P 𝑤)
37		equcom 1752	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑎 ↔ 𝑎 = 𝑤)
38		bicom 140	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎) ↔ (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
39	17, 37, 38	3imtr3i 200	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
40		simp-4r 542	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
41		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑦 ∈ 𝐴)
42	29, 41	eqeltrd 2306	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
43	1	rabeq2i 2796	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴))
44	32, 42, 43	sylanbrc 417	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤 ∈ 𝐵)
45	39, 40, 44	rspcdva 2912	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
46	36, 45	pm2.21fal 1415	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
47	27, 46	rexlimddv 2653	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
48	47	inegd 1414	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
49	48	ralrimiva 2603	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
50	49	ex 115	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
51	18, 50	biimtrid 152	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
52		nfv 1574	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑣 ∈ P)
53		nfra1 2561	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
54	52, 53	nfan 1611	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
55		nfv 1574	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ R
56	54, 55	nfan 1611	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R)
57		nfv 1574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
58	56, 57	nfan 1611	. . . . . . . . . . 11 ⊢ Ⅎ𝑤((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59		nfv 1574	. . . . . . . . . . 11 ⊢ Ⅎ𝑤(𝐶 +R -1R) <R 𝑦
60	58, 59	nfan 1611	. . . . . . . . . 10 ⊢ Ⅎ𝑤(((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦)
61		simp-6r 546	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
62		simplr 528	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑤 ∈ P)
63		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
64		simp-4r 542	. . . . . . . . . . . . . . 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 4104	. . . . . . . . . . . . . 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 548	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑣 ∈ P)
67	9	ad4antr 494	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → 𝐶 ∈ R)
68	67	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝐶 ∈ R)
69		ltpsrprg 7986	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
70	62, 66, 68, 69	syl3anc 1271	. . . . . . . . . . . . . 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 147	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑤<P 𝑣)
72		rsp 2577	. . . . . . . . . . . . 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 4086	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑏 → (𝑤<P 𝑢 ↔ 𝑤<P 𝑏))
75	74	cbvrexv 2766	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝐵 𝑤<P 𝑢 ↔ ∃𝑏 ∈ 𝐵 𝑤<P 𝑏)
76	73, 75	sylib 122	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑏 ∈ 𝐵 𝑤<P 𝑏)
77		simprl 529	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑏 ∈ 𝐵)
78		opeq1 3856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
79	78	eceq1d 6714	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
80	79	oveq2d 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
81	80	eleq1d 2298	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
82	81, 1	elrab2 2962	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ P ∧ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
83	77, 82	sylib 122	. . . . . . . . . . . . 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 114	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴)
85		simplr 528	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
86		simprr 531	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑤<P 𝑏)
87		simpllr 534	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑤 ∈ P)
88	83	simpld 112	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑏 ∈ P)
89	67	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝐶 ∈ R)
90		ltpsrprg 7986	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑏 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
91	87, 88, 89, 90	syl3anc 1271	. . . . . . . . . . . . . 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 167	. . . . . . . . . . . . 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 4106	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94		breq2 4086	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧 ↔ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
95	94	rspcev 2907	. . . . . . . . . . . 12 ⊢ (((𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴 ∧ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
96	84, 93, 95	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
97	76, 96	rexlimddv 2653	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
98		simpr 110	. . . . . . . . . . 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 147	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
101	60, 97, 100	r19.29af 2672	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
102	3	ad5antr 496	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → 𝐶 ∈ 𝐴)
103		breq2 4086	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶))
104	103	rspcev 2907	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
105	102, 104	sylancom 420	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
106		ltm1sr 7960	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ R → (𝐶 +R -1R) <R 𝐶)
107	8, 106	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 +R -1R) <R 𝐶)
108	107	ad4antr 494	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) <R 𝐶)
109	9	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝐶 ∈ R)
110		m1r 7935	. . . . . . . . . . . 12 ⊢ -1R ∈ R
111		addclsr 7936	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ R ∧ -1R ∈ R) → (𝐶 +R -1R) ∈ R)
112	109, 110, 111	sylancl 413	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) ∈ R)
113		simplr 528	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝑦 ∈ R)
114		sowlin 4410	. . . . . . . . . . . 12 ⊢ (( <R Or R ∧ ((𝐶 +R -1R) ∈ R ∧ 𝐶 ∈ R ∧ 𝑦 ∈ R)) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶)))
115	19, 114	mpan 424	. . . . . . . . . . 11 ⊢ (((𝐶 +R -1R) ∈ R ∧ 𝐶 ∈ R ∧ 𝑦 ∈ R) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦 ∨ 𝑦 <R 𝐶)))
116	112, 109, 113, 115	syl3anc 1271	. . . . . . . . . 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 803	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
119	118	ex 115	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))
120	119	ralrimiva 2603	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))
121	120	ex 115	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → (∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
122	51, 121	anim12d 335	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
123		breq1 4085	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
124	123	notbid 671	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
125	124	ralbidv 2530	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126		breq2 4086	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑦 <R 𝑥 ↔ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
127	126	imbi1d 231	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
128	127	ralbidv 2530	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
129	125, 128	anbi12d 473	. . . . 5 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
130	129	rspcev 2907	. . . 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 1476	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
132	131	rexlimdva 2648	. 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 104   ↔ wb 105   ∨ wo 713   ∧ w3a 1002   = wceq 1395  ⊥wfal 1400   ∈ wcel 2200  ∀wral 2508  ∃wrex 2509  {crab 2512   ⊆ wss 3197  ⟨cop 3669   class class class wbr 4082   Or wor 4385  (class class class)co 6000  [cec 6676  Pcnp 7474  1_Pc1p 7475  <_P cltp 7478   ~_R cer 7479  Rcnr 7480  -1_Rcm1r 7483   +_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-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-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-imp 7652  df-iltp 7653  df-enr 7909  df-nr 7910  df-plr 7911  df-mr 7912  df-ltr 7913  df-0r 7914  df-1r 7915  df-m1r 7916

This theorem is referenced by:  suplocsr  7992