ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suplocsrlem GIF version

Theorem suplocsrlem 7623
Description: Lemma for suplocsr 7624. 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.
StepHypRef 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 𝑦)))
61, 2, 3, 4, 5suplocsrlempr 7622 . 2 (𝜑 → ∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
7 simpr 109 . . . . . . 7 ((𝜑𝑣P) → 𝑣P)
82, 3sseldd 3098 . . . . . . . 8 (𝜑𝐶R)
98adantr 274 . . . . . . 7 ((𝜑𝑣P) → 𝐶R)
10 mappsrprg 7619 . . . . . . 7 ((𝑣P𝐶R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
117, 9, 10syl2anc 408 . . . . . 6 ((𝜑𝑣P) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
12 ltrelsr 7553 . . . . . . 7 <R ⊆ (R × R)
1312brel 4591 . . . . . 6 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
1411, 13syl 14 . . . . 5 ((𝜑𝑣P) → ((𝐶 +R -1R) ∈ R ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R))
1514simprd 113 . . . 4 ((𝜑𝑣P) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R)
16 breq2 3933 . . . . . . . 8 (𝑤 = 𝑎 → (𝑣<P 𝑤𝑣<P 𝑎))
1716notbid 656 . . . . . . 7 (𝑤 = 𝑎 → (¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎))
1817cbvralv 2654 . . . . . 6 (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑎𝐵 ¬ 𝑣<P 𝑎)
19 ltsosr 7579 . . . . . . . . . . . . . . 15 <R Or R
2019, 12sotri 4934 . . . . . . . . . . . . . 14 (((𝐶 +R -1R) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
2111, 20sylan 281 . . . . . . . . . . . . 13 (((𝜑𝑣P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → (𝐶 +R -1R) <R 𝑦)
229adantr 274 . . . . . . . . . . . . . 14 (((𝜑𝑣P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → 𝐶R)
23 map2psrprg 7620 . . . . . . . . . . . . . 14 (𝐶R → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
2422, 23syl 14 . . . . . . . . . . . . 13 (((𝜑𝑣P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
2521, 24mpbid 146 . . . . . . . . . . . 12 (((𝜑𝑣P) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
2625adantlr 468 . . . . . . . . . . 11 ((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
2726adantlr 468 . . . . . . . . . 10 (((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
28 simplr 519 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
29 simprr 521 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
3028, 29breqtrrd 3956 . . . . . . . . . . . 12 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ))
317ad4antr 485 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣P)
32 simprl 520 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤P)
339ad4antr 485 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝐶R)
34 ltpsrprg 7618 . . . . . . . . . . . . 13 ((𝑣P𝑤P𝐶R) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
3531, 32, 33, 34syl3anc 1216 . . . . . . . . . . . 12 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ((𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ↔ 𝑣<P 𝑤))
3630, 35mpbid 146 . . . . . . . . . . 11 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑣<P 𝑤)
37 equcom 1682 . . . . . . . . . . . . 13 (𝑤 = 𝑎𝑎 = 𝑤)
38 bicom 139 . . . . . . . . . . . . 13 ((¬ 𝑣<P 𝑤 ↔ ¬ 𝑣<P 𝑎) ↔ (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
3917, 37, 383imtr3i 199 . . . . . . . . . . . 12 (𝑎 = 𝑤 → (¬ 𝑣<P 𝑎 ↔ ¬ 𝑣<P 𝑤))
40 simp-4r 531 . . . . . . . . . . . 12 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ∀𝑎𝐵 ¬ 𝑣<P 𝑎)
41 simpllr 523 . . . . . . . . . . . . . 14 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑦𝐴)
4229, 41eqeltrd 2216 . . . . . . . . . . . . 13 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴)
431rabeq2i 2683 . . . . . . . . . . . . 13 (𝑤𝐵 ↔ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴))
4432, 42, 43sylanbrc 413 . . . . . . . . . . . 12 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → 𝑤𝐵)
4539, 40, 44rspcdva 2794 . . . . . . . . . . 11 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ¬ 𝑣<P 𝑤)
4636, 45pm2.21fal 1351 . . . . . . . . . 10 ((((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) ∧ (𝑤P ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)) → ⊥)
4727, 46rexlimddv 2554 . . . . . . . . 9 (((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) ∧ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦) → ⊥)
4847inegd 1350 . . . . . . . 8 ((((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) ∧ 𝑦𝐴) → ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
4948ralrimiva 2505 . . . . . . 7 (((𝜑𝑣P) ∧ ∀𝑎𝐵 ¬ 𝑣<P 𝑎) → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦)
5049ex 114 . . . . . 6 ((𝜑𝑣P) → (∀𝑎𝐵 ¬ 𝑣<P 𝑎 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
5118, 50syl5bi 151 . . . . 5 ((𝜑𝑣P) → (∀𝑤𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
52 nfv 1508 . . . . . . . . . . . . . 14 𝑤(𝜑𝑣P)
53 nfra1 2466 . . . . . . . . . . . . . 14 𝑤𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)
5452, 53nfan 1544 . . . . . . . . . . . . 13 𝑤((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢))
55 nfv 1508 . . . . . . . . . . . . 13 𝑤 𝑦R
5654, 55nfan 1544 . . . . . . . . . . . 12 𝑤(((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R)
57 nfv 1508 . . . . . . . . . . . 12 𝑤 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )
5856, 57nfan 1544 . . . . . . . . . . 11 𝑤((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
59 nfv 1508 . . . . . . . . . . 11 𝑤(𝐶 +R -1R) <R 𝑦
6058, 59nfan 1544 . . . . . . . . . 10 𝑤(((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦)
61 simp-6r 535 . . . . . . . . . . . . 13 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢))
62 simplr 519 . . . . . . . . . . . . 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 531 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ))
6563, 64eqbrtrd 3950 . . . . . . . . . . . . . 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 537 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑣P)
679ad4antr 485 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → 𝐶R)
6867ad2antrr 479 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝐶R)
69 ltpsrprg 7618 . . . . . . . . . . . . . . 15 ((𝑤P𝑣P𝐶R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) ↔ 𝑤<P 𝑣))
7062, 66, 68, 69syl3anc 1216 . . . . . . . . . . . . . 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 𝑣))
7165, 70mpbid 146 . . . . . . . . . . . . 13 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → 𝑤<P 𝑣)
72 rsp 2480 . . . . . . . . . . . . 13 (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → (𝑤P → (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)))
7361, 62, 71, 72syl3c 63 . . . . . . . . . . . 12 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑢𝐵 𝑤<P 𝑢)
74 breq2 3933 . . . . . . . . . . . . 13 (𝑢 = 𝑏 → (𝑤<P 𝑢𝑤<P 𝑏))
7574cbvrexv 2655 . . . . . . . . . . . 12 (∃𝑢𝐵 𝑤<P 𝑢 ↔ ∃𝑏𝐵 𝑤<P 𝑏)
7673, 75sylib 121 . . . . . . . . . . 11 ((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) → ∃𝑏𝐵 𝑤<P 𝑏)
77 simprl 520 . . . . . . . . . . . . . 14 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝑏𝐵)
78 opeq1 3705 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑏 → ⟨𝑤, 1P⟩ = ⟨𝑏, 1P⟩)
7978eceq1d 6465 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑏 → [⟨𝑤, 1P⟩] ~R = [⟨𝑏, 1P⟩] ~R )
8079oveq2d 5790 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
8180eleq1d 2208 . . . . . . . . . . . . . . 15 (𝑤 = 𝑏 → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴 ↔ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
8281, 1elrab2 2843 . . . . . . . . . . . . . 14 (𝑏𝐵 ↔ (𝑏P ∧ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
8377, 82sylib 121 . . . . . . . . . . . . 13 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → (𝑏P ∧ (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴))
8483simprd 113 . . . . . . . . . . . 12 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴)
85 simplr 519 . . . . . . . . . . . . 13 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
86 simprr 521 . . . . . . . . . . . . . 14 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝑤<P 𝑏)
87 simpllr 523 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝑤P)
8883simpld 111 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝑏P)
8967ad3antrrr 483 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝐶R)
90 ltpsrprg 7618 . . . . . . . . . . . . . . 15 ((𝑤P𝑏P𝐶R) → ((𝐶 +R [⟨𝑤, 1P⟩] ~R ) <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ) ↔ 𝑤<P 𝑏))
9187, 88, 89, 90syl3anc 1216 . . . . . . . . . . . . . 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 𝑏))
9286, 91mpbird 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 ))
9385, 92eqbrtrrd 3952 . . . . . . . . . . . 12 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → 𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R ))
94 breq2 3933 . . . . . . . . . . . . 13 (𝑧 = (𝐶 +R [⟨𝑏, 1P⟩] ~R ) → (𝑦 <R 𝑧𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )))
9594rspcev 2789 . . . . . . . . . . . 12 (((𝐶 +R [⟨𝑏, 1P⟩] ~R ) ∈ 𝐴𝑦 <R (𝐶 +R [⟨𝑏, 1P⟩] ~R )) → ∃𝑧𝐴 𝑦 <R 𝑧)
9684, 93, 95syl2anc 408 . . . . . . . . . . 11 (((((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) ∧ 𝑤P) ∧ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦) ∧ (𝑏𝐵𝑤<P 𝑏)) → ∃𝑧𝐴 𝑦 <R 𝑧)
9776, 96rexlimddv 2554 . . . . . . . . . 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 𝑦)
9967, 23syl 14 . . . . . . . . . . 11 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ((𝐶 +R -1R) <R 𝑦 ↔ ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦))
10098, 99mpbid 146 . . . . . . . . . 10 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑤P (𝐶 +R [⟨𝑤, 1P⟩] ~R ) = 𝑦)
10160, 97, 100r19.29af 2573 . . . . . . . . 9 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ (𝐶 +R -1R) <R 𝑦) → ∃𝑧𝐴 𝑦 <R 𝑧)
1023ad5antr 487 . . . . . . . . . 10 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → 𝐶𝐴)
103 breq2 3933 . . . . . . . . . . 11 (𝑧 = 𝐶 → (𝑦 <R 𝑧𝑦 <R 𝐶))
104103rspcev 2789 . . . . . . . . . 10 ((𝐶𝐴𝑦 <R 𝐶) → ∃𝑧𝐴 𝑦 <R 𝑧)
105102, 104sylancom 416 . . . . . . . . 9 ((((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) ∧ 𝑦 <R 𝐶) → ∃𝑧𝐴 𝑦 <R 𝑧)
106 ltm1sr 7592 . . . . . . . . . . . 12 (𝐶R → (𝐶 +R -1R) <R 𝐶)
1078, 106syl 14 . . . . . . . . . . 11 (𝜑 → (𝐶 +R -1R) <R 𝐶)
108107ad4antr 485 . . . . . . . . . 10 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) <R 𝐶)
1099ad3antrrr 483 . . . . . . . . . . . 12 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝐶R)
110 m1r 7567 . . . . . . . . . . . 12 -1RR
111 addclsr 7568 . . . . . . . . . . . 12 ((𝐶R ∧ -1RR) → (𝐶 +R -1R) ∈ R)
112109, 110, 111sylancl 409 . . . . . . . . . . 11 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → (𝐶 +R -1R) ∈ R)
113 simplr 519 . . . . . . . . . . 11 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → 𝑦R)
114 sowlin 4242 . . . . . . . . . . . 12 (( <R Or R ∧ ((𝐶 +R -1R) ∈ R𝐶R𝑦R)) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦𝑦 <R 𝐶)))
11519, 114mpan 420 . . . . . . . . . . 11 (((𝐶 +R -1R) ∈ R𝐶R𝑦R) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦𝑦 <R 𝐶)))
116112, 109, 113, 115syl3anc 1216 . . . . . . . . . 10 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ((𝐶 +R -1R) <R 𝐶 → ((𝐶 +R -1R) <R 𝑦𝑦 <R 𝐶)))
117108, 116mpd 13 . . . . . . . . 9 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ((𝐶 +R -1R) <R 𝑦𝑦 <R 𝐶))
118101, 105, 117mpjaodan 787 . . . . . . . 8 (((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) ∧ 𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )) → ∃𝑧𝐴 𝑦 <R 𝑧)
119118ex 114 . . . . . . 7 ((((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) ∧ 𝑦R) → (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
120119ralrimiva 2505 . . . . . 6 (((𝜑𝑣P) ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))
121120ex 114 . . . . 5 ((𝜑𝑣P) → (∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢) → ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
12251, 121anim12d 333 . . . 4 ((𝜑𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
123 breq1 3932 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑥 <R 𝑦 ↔ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
124123notbid 656 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (¬ 𝑥 <R 𝑦 ↔ ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
125124ralbidv 2437 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦))
126 breq2 3933 . . . . . . . 8 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (𝑦 <R 𝑥𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R )))
127126imbi1d 230 . . . . . . 7 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
128127ralbidv 2437 . . . . . 6 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → (∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧) ↔ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧)))
129125, 128anbi12d 464 . . . . 5 (𝑥 = (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ((∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))))
130129rspcev 2789 . . . 4 (((𝐶 +R [⟨𝑣, 1P⟩] ~R ) ∈ R ∧ (∀𝑦𝐴 ¬ (𝐶 +R [⟨𝑣, 1P⟩] ~R ) <R 𝑦 ∧ ∀𝑦R (𝑦 <R (𝐶 +R [⟨𝑣, 1P⟩] ~R ) → ∃𝑧𝐴 𝑦 <R 𝑧))) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
13115, 122, 130syl6an 1410 . . 3 ((𝜑𝑣P) → ((∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
132131rexlimdva 2549 . 2 (𝜑 → (∃𝑣P (∀𝑤𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤P (𝑤<P 𝑣 → ∃𝑢𝐵 𝑤<P 𝑢)) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧))))
1336, 132mpd 13 1 (𝜑 → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 697  w3a 962   = wceq 1331  wfal 1336  wcel 1480  wral 2416  wrex 2417  {crab 2420  wss 3071  cop 3530   class class class wbr 3929   Or wor 4217  (class class class)co 5774  [cec 6427  Pcnp 7106  1Pc1p 7107  <P cltp 7110   ~R cer 7111  Rcnr 7112  -1Rcm1r 7115   +R cplr 7116   <R cltr 7118
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-eprel 4211  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-1o 6313  df-2o 6314  df-oadd 6317  df-omul 6318  df-er 6429  df-ec 6431  df-qs 6435  df-ni 7119  df-pli 7120  df-mi 7121  df-lti 7122  df-plpq 7159  df-mpq 7160  df-enq 7162  df-nqqs 7163  df-plqqs 7164  df-mqqs 7165  df-1nqqs 7166  df-rq 7167  df-ltnqqs 7168  df-enq0 7239  df-nq0 7240  df-0nq0 7241  df-plq0 7242  df-mq0 7243  df-inp 7281  df-i1p 7282  df-iplp 7283  df-imp 7284  df-iltp 7285  df-enr 7541  df-nr 7542  df-plr 7543  df-mr 7544  df-ltr 7545  df-0r 7546  df-1r 7547  df-m1r 7548
This theorem is referenced by:  suplocsr  7624
  Copyright terms: Public domain W3C validator