Theorem suplocsrlem 8027

Description: Lemma for suplocsr 8028. 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 8026	. 2 ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
7		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝑣 ∈ P)
8	2, 3	sseldd 3228	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ R)
9	8	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝐶 ∈ R)
10		mappsrprg 8023	. . . . . . 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 7957	. . . . . . 7 ⊢ <R ⊆ (R × R)
13	12	brel 4778	. . . . . 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 4092	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑣<P 𝑤 ↔ 𝑣<P 𝑎))
17	16	notbid 673	. . . . . . 7 ⊢ (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
18	17	cbvralv 2767	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
19		ltsosr 7983	. . . . . . . . . . . . . . 15 ⊢ <R Or R
20	19, 12	sotri 5132	. . . . . . . . . . . . . 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 8024	. . . . . . . . . . . . . 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 529	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
29		simprr 533	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
30	28, 29	breqtrrd 4116	. . . . . . . . . . . 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 531	. . . . . . . . . . . . 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 8022	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ P ∧ 𝑤 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
35	31, 32, 33, 34	syl3anc 1273	. . . . . . . . . . . 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 1754	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑎 ↔ 𝑎 = 𝑤)
38		bicom 140	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎) ↔ (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
39	17, 37, 38	3imtr3i 200	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
40		simp-4r 544	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
41		simpllr 536	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑦 ∈ 𝐴)
42	29, 41	eqeltrd 2308	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
43	1	rabeq2i 2799	. . . . . . . . . . . . 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 2915	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
46	36, 45	pm2.21fal 1417	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
47	27, 46	rexlimddv 2655	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
48	47	inegd 1416	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
49	48	ralrimiva 2605	. . . . . . 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 1576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑣 ∈ P)
53		nfra1 2563	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
54	52, 53	nfan 1613	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
55		nfv 1576	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ R
56	54, 55	nfan 1613	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R)
57		nfv 1576	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
58	56, 57	nfan 1613	. . . . . . . . . . 11 ⊢ Ⅎ𝑤((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59		nfv 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑤(𝐶 +R -1R) <R 𝑦
60	58, 59	nfan 1613	. . . . . . . . . 10 ⊢ Ⅎ𝑤(((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦)
61		simp-6r 548	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
62		simplr 529	. . . . . . . . . . . . 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 544	. . . . . . . . . . . . . . 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 4110	. . . . . . . . . . . . . 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 550	. . . . . . . . . . . . . . 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 8022	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
70	62, 66, 68, 69	syl3anc 1273	. . . . . . . . . . . . . 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 2579	. . . . . . . . . . . . 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 4092	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑏 → (𝑤<P 𝑢 ↔ 𝑤<P 𝑏))
75	74	cbvrexv 2768	. . . . . . . . . . . 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 531	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑏 ∈ 𝐵)
78		opeq1 3862	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
79	78	eceq1d 6737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
80	79	oveq2d 6033	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
81	80	eleq1d 2300	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
82	81, 1	elrab2 2965	. . . . . . . . . . . . . 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 529	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
86		simprr 533	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑤<P 𝑏)
87		simpllr 536	. . . . . . . . . . . . . . 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 8022	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑏 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
91	87, 88, 89, 90	syl3anc 1273	. . . . . . . . . . . . . 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 4112	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94		breq2 4092	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧 ↔ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
95	94	rspcev 2910	. . . . . . . . . . . 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 2655	. . . . . . . . . 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 2674	. . . . . . . . 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 4092	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶))
104	103	rspcev 2910	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
105	102, 104	sylancom 420	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
106		ltm1sr 7996	. . . . . . . . . . . 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 7971	. . . . . . . . . . . 12 ⊢ -1R ∈ R
111		addclsr 7972	. . . . . . . . . . . 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 529	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝑦 ∈ R)
114		sowlin 4417	. . . . . . . . . . . 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 1273	. . . . . . . . . 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 805	. . . . . . . 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 2605	. . . . . 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 4091	. . . . . . . 8 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
124	123	notbid 673	. . . . . . 7 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
125	124	ralbidv 2532	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126		breq2 4092	. . . . . . . 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 2532	. . . . . 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 2910	. . . 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 1478	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
132	131	rexlimdva 2650	. 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 715   ∧ w3a 1004   = wceq 1397  ⊥wfal 1402   ∈ wcel 2202  ∀wral 2510  ∃wrex 2511  {crab 2514   ⊆ wss 3200  ⟨cop 3672   class class class wbr 4088   Or wor 4392  (class class class)co 6017  [cec 6699  Pcnp 7510  1_Pc1p 7511  <_P cltp 7514   ~_R cer 7515  Rcnr 7516  -1_Rcm1r 7519   +_R cplr 7520   <_R cltr 7522

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-eprel 4386  df-id 4390  df-po 4393  df-iso 4394  df-iord 4463  df-on 4465  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-ov 6020  df-oprab 6021  df-mpo 6022  df-1st 6302  df-2nd 6303  df-recs 6470  df-irdg 6535  df-1o 6581  df-2o 6582  df-oadd 6585  df-omul 6586  df-er 6701  df-ec 6703  df-qs 6707  df-ni 7523  df-pli 7524  df-mi 7525  df-lti 7526  df-plpq 7563  df-mpq 7564  df-enq 7566  df-nqqs 7567  df-plqqs 7568  df-mqqs 7569  df-1nqqs 7570  df-rq 7571  df-ltnqqs 7572  df-enq0 7643  df-nq0 7644  df-0nq0 7645  df-plq0 7646  df-mq0 7647  df-inp 7685  df-i1p 7686  df-iplp 7687  df-imp 7688  df-iltp 7689  df-enr 7945  df-nr 7946  df-plr 7947  df-mr 7948  df-ltr 7949  df-0r 7950  df-1r 7951  df-m1r 7952

This theorem is referenced by:  suplocsr  8028