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
 Copyright terms: Public domain W3C validator