Theorem suplocsrlem 7868

Description: Lemma for suplocsr 7869. 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 7867	. 2 ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
7		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝑣 ∈ P)
8	2, 3	sseldd 3180	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ R)
9	8	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝐶 ∈ R)
10		mappsrprg 7864	. . . . . . 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 7798	. . . . . . 7 ⊢ <R ⊆ (R × R)
13	12	brel 4711	. . . . . 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 4033	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑣<P 𝑤 ↔ 𝑣<P 𝑎))
17	16	notbid 668	. . . . . . 7 ⊢ (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
18	17	cbvralv 2726	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
19		ltsosr 7824	. . . . . . . . . . . . . . 15 ⊢ <R Or R
20	19, 12	sotri 5061	. . . . . . . . . . . . . 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 7865	. . . . . . . . . . . . . 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 4057	. . . . . . . . . . . 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 7863	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ P ∧ 𝑤 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
35	31, 32, 33, 34	syl3anc 1249	. . . . . . . . . . . 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 1717	. . . . . . . . . . . . 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 2270	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
43	1	rabeq2i 2757	. . . . . . . . . . . . 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 2869	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
46	36, 45	pm2.21fal 1384	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
47	27, 46	rexlimddv 2616	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
48	47	inegd 1383	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
49	48	ralrimiva 2567	. . . . . . 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 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑣 ∈ P)
53		nfra1 2525	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
54	52, 53	nfan 1576	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
55		nfv 1539	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ R
56	54, 55	nfan 1576	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R)
57		nfv 1539	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
58	56, 57	nfan 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑤((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59		nfv 1539	. . . . . . . . . . 11 ⊢ Ⅎ𝑤(𝐶 +R -1R) <R 𝑦
60	58, 59	nfan 1576	. . . . . . . . . 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 4051	. . . . . . . . . . . . . 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 7863	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
70	62, 66, 68, 69	syl3anc 1249	. . . . . . . . . . . . . 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 2541	. . . . . . . . . . . . 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 4033	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑏 → (𝑤<P 𝑢 ↔ 𝑤<P 𝑏))
75	74	cbvrexv 2727	. . . . . . . . . . . 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 3804	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
79	78	eceq1d 6623	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
80	79	oveq2d 5934	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
81	80	eleq1d 2262	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
82	81, 1	elrab2 2919	. . . . . . . . . . . . . 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 7863	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑏 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
91	87, 88, 89, 90	syl3anc 1249	. . . . . . . . . . . . . 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 4053	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94		breq2 4033	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧 ↔ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
95	94	rspcev 2864	. . . . . . . . . . . 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 2616	. . . . . . . . . 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 2635	. . . . . . . . 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 4033	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶))
104	103	rspcev 2864	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
105	102, 104	sylancom 420	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
106		ltm1sr 7837	. . . . . . . . . . . 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 7812	. . . . . . . . . . . 12 ⊢ -1R ∈ R
111		addclsr 7813	. . . . . . . . . . . 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 4351	. . . . . . . . . . . 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 1249	. . . . . . . . . 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 799	. . . . . . . 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 2567	. . . . . 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 4032	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
124	123	notbid 668	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
125	124	ralbidv 2494	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126		breq2 4033	. . . . . . . 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 2494	. . . . . 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 2864	. . . 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 1445	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
132	131	rexlimdva 2611	. 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 709   ∧ w3a 980   = wceq 1364  ⊥wfal 1369   ∈ wcel 2164  ∀wral 2472  ∃wrex 2473  {crab 2476   ⊆ wss 3153  ⟨cop 3621   class class class wbr 4029   Or wor 4326  (class class class)co 5918  [cec 6585  Pcnp 7351  1_Pc1p 7352  <_P cltp 7355   ~_R cer 7356  Rcnr 7357  -1_Rcm1r 7360   +_R cplr 7361   <_R cltr 7363

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-eprel 4320  df-id 4324  df-po 4327  df-iso 4328  df-iord 4397  df-on 4399  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-recs 6358  df-irdg 6423  df-1o 6469  df-2o 6470  df-oadd 6473  df-omul 6474  df-er 6587  df-ec 6589  df-qs 6593  df-ni 7364  df-pli 7365  df-mi 7366  df-lti 7367  df-plpq 7404  df-mpq 7405  df-enq 7407  df-nqqs 7408  df-plqqs 7409  df-mqqs 7410  df-1nqqs 7411  df-rq 7412  df-ltnqqs 7413  df-enq0 7484  df-nq0 7485  df-0nq0 7486  df-plq0 7487  df-mq0 7488  df-inp 7526  df-i1p 7527  df-iplp 7528  df-imp 7529  df-iltp 7530  df-enr 7786  df-nr 7787  df-plr 7788  df-mr 7789  df-ltr 7790  df-0r 7791  df-1r 7792  df-m1r 7793

This theorem is referenced by:  suplocsr  7869