This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supsrlem

Description: Lemma for supremum theorem. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses supsrlem.1 ⊢ 𝐵 = { 𝑤 ∣ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 }
supsrlem.2 ⊢ 𝐶 ∈ R
Assertion supsrlem ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 supsrlem.1 ⊢ 𝐵 = { 𝑤 ∣ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 }
2 supsrlem.2 ⊢ 𝐶 ∈ R
3 0idsr ⊢ ( 𝐶 ∈ R → ( 𝐶 +R 0R ) = 𝐶 )
4 2 3 mp1i ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ( 𝐶 +R 0R ) = 𝐶 )
5 simpl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → 𝐶 ∈ 𝐴 )
6 4 5 eqeltrd ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ( 𝐶 +R 0R ) ∈ 𝐴 )
7 1pr ⊢ 1P ∈ P
8 7 elexi ⊢ 1P ∈ V
9 opeq1 ⊢ ( 𝑤 = 1P → ⟨ 𝑤 , 1P ⟩ = ⟨ 1P , 1P ⟩ )
10 9 eceq1d ⊢ ( 𝑤 = 1P → [ ⟨ 𝑤 , 1P ⟩ ] ~R = [ ⟨ 1P , 1P ⟩ ] ~R )
11 df-0r ⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
12 10 11 eqtr4di ⊢ ( 𝑤 = 1P → [ ⟨ 𝑤 , 1P ⟩ ] ~R = 0R )
13 12 oveq2d ⊢ ( 𝑤 = 1P → ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = ( 𝐶 +R 0R ) )
14 13 eleq1d ⊢ ( 𝑤 = 1P → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 ↔ ( 𝐶 +R 0R ) ∈ 𝐴 ) )
15 8 14 1 elab2 ⊢ ( 1P ∈ 𝐵 ↔ ( 𝐶 +R 0R ) ∈ 𝐴 )
16 6 15 sylibr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → 1P ∈ 𝐵 )
17 16 ne0d ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → 𝐵 ≠ ∅ )
18 breq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 <R 𝑥 ↔ 𝐶 <R 𝑥 ) )
19 18 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝐶 ∈ 𝐴 → 𝐶 <R 𝑥 ) )
20 0lt1sr ⊢ 0R <R 1R
21 m1r ⊢ -1R ∈ R
22 ltasr ⊢ ( -1R ∈ R → ( 0R <R 1R ↔ ( -1R +R 0R ) <R ( -1R +R 1R ) ) )
23 21 22 ax-mp ⊢ ( 0R <R 1R ↔ ( -1R +R 0R ) <R ( -1R +R 1R ) )
24 20 23 mpbi ⊢ ( -1R +R 0R ) <R ( -1R +R 1R )
25 0idsr ⊢ ( -1R ∈ R → ( -1R +R 0R ) = -1R )
26 21 25 ax-mp ⊢ ( -1R +R 0R ) = -1R
27 m1p1sr ⊢ ( -1R +R 1R ) = 0R
28 24 26 27 3brtr3i ⊢ -1R <R 0R
29 ltasr ⊢ ( 𝐶 ∈ R → ( -1R <R 0R ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R 0R ) ) )
30 2 29 ax-mp ⊢ ( -1R <R 0R ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R 0R ) )
31 28 30 mpbi ⊢ ( 𝐶 +R -1R ) <R ( 𝐶 +R 0R )
32 2 3 ax-mp ⊢ ( 𝐶 +R 0R ) = 𝐶
33 31 32 breqtri ⊢ ( 𝐶 +R -1R ) <R 𝐶
34 ltsosr ⊢ <R Or R
35 ltrelsr ⊢ <R ⊆ ( R × R )
36 34 35 sotri ⊢ ( ( ( 𝐶 +R -1R ) <R 𝐶 ∧ 𝐶 <R 𝑥 ) → ( 𝐶 +R -1R ) <R 𝑥 )
37 33 36 mpan ⊢ ( 𝐶 <R 𝑥 → ( 𝐶 +R -1R ) <R 𝑥 )
38 2 map2psrpr ⊢ ( ( 𝐶 +R -1R ) <R 𝑥 ↔ ∃ 𝑣 ∈ P ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 )
39 37 38 sylib ⊢ ( 𝐶 <R 𝑥 → ∃ 𝑣 ∈ P ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 )
40 19 39 syl6 ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝐶 ∈ 𝐴 → ∃ 𝑣 ∈ P ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 ) )
41 breq2 ⊢ ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ 𝑦 <R 𝑥 ) )
42 41 ralbidv ⊢ ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) )
43 1 eqabri ⊢ ( 𝑤 ∈ 𝐵 ↔ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 )
44 breq1 ⊢ ( 𝑦 = ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ) )
45 44 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 → ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ) )
46 2 ltpsrpr ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ 𝑤 <P 𝑣 )
47 45 46 imbitrdi ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 → 𝑤 <P 𝑣 ) )
48 43 47 biimtrid ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( 𝑤 ∈ 𝐵 → 𝑤 <P 𝑣 ) )
49 48 ralrimiv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 )
50 42 49 biimtrrdi ⊢ ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) )
51 50 com12 ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 → ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) )
52 51 reximdv ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( ∃ 𝑣 ∈ P ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = 𝑥 → ∃ 𝑣 ∈ P ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) )
53 40 52 syld ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝐶 ∈ 𝐴 → ∃ 𝑣 ∈ P ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) )
54 53 rexlimivw ⊢ ( ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝐶 ∈ 𝐴 → ∃ 𝑣 ∈ P ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) )
55 54 impcom ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑣 ∈ P ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 )
56 supexpr ⊢ ( ( 𝐵 ≠ ∅ ∧ ∃ 𝑣 ∈ P ∀ 𝑤 ∈ 𝐵 𝑤 <P 𝑣 ) → ∃ 𝑣 ∈ P ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) )
57 17 55 56 syl2anc ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑣 ∈ P ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) )
58 2 mappsrpr ⊢ ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ 𝑣 ∈ P )
59 35 brel ⊢ ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R -1R ) ∈ R ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ R ) )
60 58 59 sylbir ⊢ ( 𝑣 ∈ P → ( ( 𝐶 +R -1R ) ∈ R ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ R ) )
61 60 simprd ⊢ ( 𝑣 ∈ P → ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ R )
62 61 adantl ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ∧ 𝑣 ∈ P ) → ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ R )
63 34 35 sotri ⊢ ( ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) → ( 𝐶 +R -1R ) <R 𝑦 )
64 58 63 sylanbr ⊢ ( ( 𝑣 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) → ( 𝐶 +R -1R ) <R 𝑦 )
65 2 map2psrpr ⊢ ( ( 𝐶 +R -1R ) <R 𝑦 ↔ ∃ 𝑤 ∈ P ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 )
66 64 65 sylib ⊢ ( ( 𝑣 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) → ∃ 𝑤 ∈ P ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 )
67 rexex ⊢ ( ∃ 𝑤 ∈ P ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ∃ 𝑤 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 )
68 df-ral ⊢ ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) )
69 19.29 ⊢ ( ( ∀ 𝑤 ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ∧ ∃ 𝑤 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ∃ 𝑤 ( ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) )
70 eleq1 ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
71 43 70 bitrid ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( 𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐴 ) )
72 2 ltpsrpr ⊢ ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ↔ 𝑣 <P 𝑤 )
73 breq2 ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ↔ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
74 72 73 bitr3id ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( 𝑣 <P 𝑤 ↔ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
75 74 notbid ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ¬ 𝑣 <P 𝑤 ↔ ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
76 71 75 imbi12d ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ↔ ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) ) )
77 76 biimpac ⊢ ( ( ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
78 77 exlimiv ⊢ ( ∃ 𝑤 ( ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
79 69 78 syl ⊢ ( ( ∀ 𝑤 ( 𝑤 ∈ 𝐵 → ¬ 𝑣 <P 𝑤 ) ∧ ∃ 𝑤 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
80 68 79 sylanb ⊢ ( ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∃ 𝑤 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
81 80 expcom ⊢ ( ∃ 𝑤 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) ) )
82 66 67 81 3syl ⊢ ( ( 𝑣 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) ) )
83 82 impd ⊢ ( ( 𝑣 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) → ( ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ 𝑦 ∈ 𝐴 ) → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
84 83 impancom ⊢ ( ( 𝑣 ∈ P ∧ ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
85 84 pm2.01d ⊢ ( ( 𝑣 ∈ P ∧ ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ 𝑦 ∈ 𝐴 ) ) → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 )
86 85 expr ⊢ ( ( 𝑣 ∈ P ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ) → ( 𝑦 ∈ 𝐴 → ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
87 86 ralrimiv ⊢ ( ( 𝑣 ∈ P ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ) → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 )
88 87 ex ⊢ ( 𝑣 ∈ P → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
89 88 adantl ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ∧ 𝑣 ∈ P ) → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
90 r19.29 ⊢ ( ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ∃ 𝑤 ∈ P ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ∃ 𝑤 ∈ P ( ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) )
91 breq1 ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ↔ 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ) )
92 46 91 bitr3id ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( 𝑤 <P 𝑣 ↔ 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ) )
93 92 biimprd ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → 𝑤 <P 𝑣 ) )
94 vex ⊢ 𝑢 ∈ V
95 opeq1 ⊢ ( 𝑤 = 𝑢 → ⟨ 𝑤 , 1P ⟩ = ⟨ 𝑢 , 1P ⟩ )
96 95 eceq1d ⊢ ( 𝑤 = 𝑢 → [ ⟨ 𝑤 , 1P ⟩ ] ~R = [ ⟨ 𝑢 , 1P ⟩ ] ~R )
97 96 oveq2d ⊢ ( 𝑤 = 𝑢 → ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) )
98 97 eleq1d ⊢ ( 𝑤 = 𝑢 → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 ↔ ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) ∈ 𝐴 ) )
99 94 98 1 elab2 ⊢ ( 𝑢 ∈ 𝐵 ↔ ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) ∈ 𝐴 )
100 breq2 ⊢ ( 𝑧 = ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 ↔ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) ) )
101 2 ltpsrpr ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) ↔ 𝑤 <P 𝑢 )
102 100 101 bitrdi ⊢ ( 𝑧 = ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 ↔ 𝑤 <P 𝑢 ) )
103 102 rspcev ⊢ ( ( ( 𝐶 +R [ ⟨ 𝑢 , 1P ⟩ ] ~R ) ∈ 𝐴 ∧ 𝑤 <P 𝑢 ) → ∃ 𝑧 ∈ 𝐴 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 )
104 99 103 sylanb ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 <P 𝑢 ) → ∃ 𝑧 ∈ 𝐴 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 )
105 104 rexlimiva ⊢ ( ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 → ∃ 𝑧 ∈ 𝐴 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 )
106 breq1 ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 ↔ 𝑦 <R 𝑧 ) )
107 106 rexbidv ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ∃ 𝑧 ∈ 𝐴 ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) <R 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
108 105 107 imbitrid ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
109 93 108 imim12d ⊢ ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 → ( ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
110 109 impcom ⊢ ( ( ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
111 110 rexlimivw ⊢ ( ∃ 𝑤 ∈ P ( ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
112 90 111 syl ⊢ ( ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ∃ 𝑤 ∈ P ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) = 𝑦 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
113 65 112 sylan2b ⊢ ( ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ∧ ( 𝐶 +R -1R ) <R 𝑦 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
114 113 ex ⊢ ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) → ( ( 𝐶 +R -1R ) <R 𝑦 → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
115 114 adantl ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ( ( 𝐶 +R -1R ) <R 𝑦 → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
116 115 a1dd ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ( ( 𝐶 +R -1R ) <R 𝑦 → ( 𝑦 ∈ R → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
117 34 35 sotri2 ⊢ ( ( 𝑦 ∈ R ∧ ¬ ( 𝐶 +R -1R ) <R 𝑦 ∧ ( 𝐶 +R -1R ) <R 𝐶 ) → 𝑦 <R 𝐶 )
118 33 117 mp3an3 ⊢ ( ( 𝑦 ∈ R ∧ ¬ ( 𝐶 +R -1R ) <R 𝑦 ) → 𝑦 <R 𝐶 )
119 breq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶 ) )
120 119 rspcev ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶 ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 )
121 120 ex ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 <R 𝐶 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
122 121 a1dd ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 <R 𝐶 → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
123 118 122 syl5 ⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝑦 ∈ R ∧ ¬ ( 𝐶 +R -1R ) <R 𝑦 ) → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
124 123 expcomd ⊢ ( 𝐶 ∈ 𝐴 → ( ¬ ( 𝐶 +R -1R ) <R 𝑦 → ( 𝑦 ∈ R → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
125 124 ad2antrr ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ( ¬ ( 𝐶 +R -1R ) <R 𝑦 → ( 𝑦 ∈ R → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
126 116 125 pm2.61d ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ( 𝑦 ∈ R → ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
127 126 ralrimiv ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) )
128 127 ex ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P ) → ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) → ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
129 128 adantlr ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ∧ 𝑣 ∈ P ) → ( ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) → ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
130 89 129 anim12d ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ∧ 𝑣 ∈ P ) → ( ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ( ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
131 breq1 ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( 𝑥 <R 𝑦 ↔ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
132 131 notbid ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ¬ 𝑥 <R 𝑦 ↔ ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
133 132 ralbidv ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ) )
134 breq2 ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( 𝑦 <R 𝑥 ↔ 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ) )
135 134 imbi1d ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ↔ ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
136 135 ralbidv ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ↔ ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
137 133 136 anbi12d ⊢ ( 𝑥 = ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
138 137 rspcev ⊢ ( ( ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ R ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
139 62 130 138 syl6an ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ∧ 𝑣 ∈ P ) → ( ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
140 139 rexlimdva ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ( ∃ 𝑣 ∈ P ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 <P 𝑤 ∧ ∀ 𝑤 ∈ P ( 𝑤 <P 𝑣 → ∃ 𝑢 ∈ 𝐵 𝑤 <P 𝑢 ) ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
141 57 140 mpd ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )