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 B = w | C + 𝑹 w 1 𝑷 ~ 𝑹 A
supsrlem.2 C 𝑹
Assertion supsrlem C A x 𝑹 y A y < 𝑹 x x 𝑹 y A ¬ x < 𝑹 y y 𝑹 y < 𝑹 x z A y < 𝑹 z

Proof

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