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 1PP
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 -1RR
22 ltasr ( -1RR → ( 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 ( -1RR → ( -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 abeq2i ( 𝑤𝐵 ↔ ( 𝐶 +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 syl6ib ( ∀ 𝑦𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( ( 𝐶 +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴𝑤 <P 𝑣 ) )
48 43 47 syl5bi ( ∀ 𝑦𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ( 𝑤𝐵𝑤 <P 𝑣 ) )
49 48 ralrimiv ( ∀ 𝑦𝐴 𝑦 <R ( 𝐶 +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) → ∀ 𝑤𝐵 𝑤 <P 𝑣 )
50 42 49 syl6bir ( ( 𝐶 +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 syl5bb ( ( 𝐶 +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 syl5ib ( ( 𝐶 +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 𝑧 ) ) )