Theorem suplocsrlem 8071

Description: Lemma for suplocsr 8072. 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 8070	. 2 ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
7		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝑣 ∈ P)
8	2, 3	sseldd 3229	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ R)
9	8	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → 𝐶 ∈ R)
10		mappsrprg 8067	. . . . . . 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 8001	. . . . . . 7 ⊢ <R ⊆ (R × R)
13	12	brel 4784	. . . . . 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 4097	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑣<P 𝑤 ↔ 𝑣<P 𝑎))
17	16	notbid 673	. . . . . . 7 ⊢ (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
18	17	cbvralv 2768	. . . . . 6 ⊢ (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎)
19		ltsosr 8027	. . . . . . . . . . . . . . 15 ⊢ <R Or R
20	19, 12	sotri 5139	. . . . . . . . . . . . . 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 8068	. . . . . . . . . . . . . 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 4121	. . . . . . . . . . . 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 8066	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ P ∧ 𝑤 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
35	31, 32, 33, 34	syl3anc 1274	. . . . . . . . . . . 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 2800	. . . . . . . . . . . . 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 2916	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
46	36, 45	pm2.21fal 1418	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤 ∈ P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
47	27, 46	rexlimddv 2656	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
48	47	inegd 1417	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑎 ∈ 𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
49	48	ralrimiva 2606	. . . . . . 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 1577	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑣 ∈ P)
53		nfra1 2564	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)
54	52, 53	nfan 1614	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))
55		nfv 1577	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤 𝑦 ∈ R
56	54, 55	nfan 1614	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R)
57		nfv 1577	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
58	56, 57	nfan 1614	. . . . . . . . . . 11 ⊢ Ⅎ𝑤((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59		nfv 1577	. . . . . . . . . . 11 ⊢ Ⅎ𝑤(𝐶 +R -1R) <R 𝑦
60	58, 59	nfan 1614	. . . . . . . . . 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 4115	. . . . . . . . . . . . . 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 8066	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
70	62, 66, 68, 69	syl3anc 1274	. . . . . . . . . . . . . 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 2580	. . . . . . . . . . . . 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 4097	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑏 → (𝑤<P 𝑢 ↔ 𝑤<P 𝑏))
75	74	cbvrexv 2769	. . . . . . . . . . . 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 3867	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
79	78	eceq1d 6781	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
80	79	oveq2d 6044	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
81	80	eleq1d 2300	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
82	81, 1	elrab2 2966	. . . . . . . . . . . . . 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 8066	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ P ∧ 𝑏 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
91	87, 88, 89, 90	syl3anc 1274	. . . . . . . . . . . . . 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 4117	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤 ∈ P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏 ∈ 𝐵 ∧ 𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94		breq2 4097	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧 ↔ 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
95	94	rspcev 2911	. . . . . . . . . . . 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 2656	. . . . . . . . . 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 2675	. . . . . . . . 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 4097	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶))
104	103	rspcev 2911	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
105	102, 104	sylancom 420	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) ∧ 𝑦 ∈ R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)
106		ltm1sr 8040	. . . . . . . . . . . 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 8015	. . . . . . . . . . . 12 ⊢ -1R ∈ R
111		addclsr 8016	. . . . . . . . . . . 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 4423	. . . . . . . . . . . 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 1274	. . . . . . . . . 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 806	. . . . . . . 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 2606	. . . . . 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 4096	. . . . . . . 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 2533	. . . . . 6 ⊢ (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126		breq2 4097	. . . . . . . 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 2533	. . . . . 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 2911	. . . 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 1479	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ P) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))
132	131	rexlimdva 2651	. 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 716   ∧ w3a 1005   = wceq 1398  ⊥wfal 1403   ∈ wcel 2202  ∀wral 2511  ∃wrex 2512  {crab 2515   ⊆ wss 3201  ⟨cop 3676   class class class wbr 4093   Or wor 4398  (class class class)co 6028  [cec 6743  Pcnp 7554  1_Pc1p 7555  <_P cltp 7558   ~_R cer 7559  Rcnr 7560  -1_Rcm1r 7563   +_R cplr 7564   <_R cltr 7566

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4209  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-iinf 4692

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-csb 3129  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-iun 3977  df-br 4094  df-opab 4156  df-mpt 4157  df-tr 4193  df-eprel 4392  df-id 4396  df-po 4399  df-iso 4400  df-iord 4469  df-on 4471  df-suc 4474  df-iom 4695  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340  df-fv 5341  df-ov 6031  df-oprab 6032  df-mpo 6033  df-1st 6312  df-2nd 6313  df-recs 6514  df-irdg 6579  df-1o 6625  df-2o 6626  df-oadd 6629  df-omul 6630  df-er 6745  df-ec 6747  df-qs 6751  df-ni 7567  df-pli 7568  df-mi 7569  df-lti 7570  df-plpq 7607  df-mpq 7608  df-enq 7610  df-nqqs 7611  df-plqqs 7612  df-mqqs 7613  df-1nqqs 7614  df-rq 7615  df-ltnqqs 7616  df-enq0 7687  df-nq0 7688  df-0nq0 7689  df-plq0 7690  df-mq0 7691  df-inp 7729  df-i1p 7730  df-iplp 7731  df-imp 7732  df-iltp 7733  df-enr 7989  df-nr 7990  df-plr 7991  df-mr 7992  df-ltr 7993  df-0r 7994  df-1r 7995  df-m1r 7996

This theorem is referenced by:  suplocsr  8072