Step | Hyp | Ref
| Expression |
1 | | xrltnr 9709 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 < 𝑥) |
2 | 1 | adantl 275 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ*) → ¬ 𝑥 < 𝑥) |
3 | | xrlttr 9725 |
. . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) |
4 | 3 | adantl 275 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*))
→ ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) |
5 | 2, 4 | ispod 4279 |
. . 3
⊢ (⊤
→ < Po ℝ*) |
6 | 5 | mptru 1351 |
. 2
⊢ < Po
ℝ* |
7 | | elxr 9706 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
↔ (𝑥 ∈ ℝ
∨ 𝑥 = +∞ ∨
𝑥 =
-∞)) |
8 | | elxr 9706 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
↔ (𝑦 ∈ ℝ
∨ 𝑦 = +∞ ∨
𝑦 =
-∞)) |
9 | | elxr 9706 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ*
↔ (𝑧 ∈ ℝ
∨ 𝑧 = +∞ ∨
𝑧 =
-∞)) |
10 | | simplr 520 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝑥 ∈
ℝ) |
11 | | simpll 519 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝑦 ∈
ℝ) |
12 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
13 | | axltwlin 7960 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
14 | 10, 11, 12, 13 | syl3anc 1227 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
15 | | ltpnf 9710 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
16 | 15 | ad2antlr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → 𝑥 < +∞) |
17 | | breq2 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = +∞ → (𝑥 < 𝑧 ↔ 𝑥 < +∞)) |
18 | 17 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑧 ↔ 𝑥 < +∞)) |
19 | 16, 18 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → 𝑥 < 𝑧) |
20 | 19 | orcd 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
21 | 20 | a1d 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
22 | | mnflt 9713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ → -∞
< 𝑦) |
23 | 22 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → -∞
< 𝑦) |
24 | | breq1 3982 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = -∞ → (𝑧 < 𝑦 ↔ -∞ < 𝑦)) |
25 | 24 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → (𝑧 < 𝑦 ↔ -∞ < 𝑦)) |
26 | 23, 25 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → 𝑧 < 𝑦) |
27 | 26 | olcd 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
28 | 27 | a1d 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
29 | 14, 21, 28 | 3jaodan 1295 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞ ∨ 𝑧 = -∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
30 | 9, 29 | sylan2b 285 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ*)
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
31 | 30 | anasss 397 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*))
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
32 | 31 | ancoms 266 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 ∈ ℝ)
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
33 | | ltpnf 9710 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℝ → 𝑧 < +∞) |
34 | 33 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝑧 < +∞) |
35 | | breq2 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = +∞ → (𝑧 < 𝑦 ↔ 𝑧 < +∞)) |
36 | 35 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝑧 < 𝑦 ↔ 𝑧 < +∞)) |
37 | 34, 36 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝑧 < 𝑦) |
38 | 37 | olcd 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
39 | 38 | a1d 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
40 | 15 | ad2antlr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → 𝑥 < +∞) |
41 | 17 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑧 ↔ 𝑥 < +∞)) |
42 | 40, 41 | mpbird 166 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → 𝑥 < 𝑧) |
43 | 42 | orcd 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
44 | 43 | a1d 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = +∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
45 | | mnfltpnf 9715 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
< +∞ |
46 | | breq12 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 = -∞ ∧ 𝑦 = +∞) → (𝑧 < 𝑦 ↔ -∞ <
+∞)) |
47 | 46 | ancoms 266 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 = +∞ ∧ 𝑧 = -∞) → (𝑧 < 𝑦 ↔ -∞ <
+∞)) |
48 | 45, 47 | mpbiri 167 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = +∞ ∧ 𝑧 = -∞) → 𝑧 < 𝑦) |
49 | 48 | adantlr 469 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → 𝑧 < 𝑦) |
50 | 49 | olcd 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
51 | 50 | a1d 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 = -∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
52 | 39, 44, 51 | 3jaodan 1295 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞ ∨ 𝑧 = -∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
53 | 9, 52 | sylan2b 285 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = +∞ ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℝ*)
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
54 | 53 | anasss 397 |
. . . . . . . . . . . 12
⊢ ((𝑦 = +∞ ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*))
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
55 | 54 | ancoms 266 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 = +∞) →
(𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
56 | | rexr 7938 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
57 | | nltmnf 9718 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ*
→ ¬ 𝑥 <
-∞) |
58 | 56, 57 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → ¬
𝑥 <
-∞) |
59 | 58 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 = -∞) →
¬ 𝑥 <
-∞) |
60 | | breq2 3983 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = -∞ → (𝑥 < 𝑦 ↔ 𝑥 < -∞)) |
61 | 60 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 = -∞) →
(𝑥 < 𝑦 ↔ 𝑥 < -∞)) |
62 | 59, 61 | mtbird 663 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 = -∞) →
¬ 𝑥 < 𝑦) |
63 | 62 | pm2.21d 609 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 = -∞) →
(𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
64 | 32, 55, 63 | 3jaodan 1295 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ (𝑦 ∈ ℝ
∨ 𝑦 = +∞ ∨
𝑦 = -∞)) →
(𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
65 | 8, 64 | sylan2b 285 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ*)
∧ 𝑦 ∈
ℝ*) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
66 | 65 | anasss 397 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ (𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
67 | 66 | ancoms 266 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ∈ ℝ) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
68 | | pnfnlt 9717 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ < 𝑦) |
69 | 68 | ad2antlr 481 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = +∞) → ¬ +∞ < 𝑦) |
70 | | breq1 3982 |
. . . . . . . . . 10
⊢ (𝑥 = +∞ → (𝑥 < 𝑦 ↔ +∞ < 𝑦)) |
71 | 70 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = +∞) → (𝑥 < 𝑦 ↔ +∞ < 𝑦)) |
72 | 69, 71 | mtbird 663 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = +∞) → ¬ 𝑥 < 𝑦) |
73 | 72 | pm2.21d 609 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = +∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
74 | | df-3or 968 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∨ 𝑧 = +∞ ∨ 𝑧 = -∞) ↔ ((𝑧 ∈ ℝ ∨ 𝑧 = +∞) ∨ 𝑧 = -∞)) |
75 | 9, 74 | bitri 183 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ*
↔ ((𝑧 ∈ ℝ
∨ 𝑧 = +∞) ∨
𝑧 =
-∞)) |
76 | | mnfltxr 9716 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℝ ∨ 𝑧 = +∞) → -∞
< 𝑧) |
77 | 76 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = -∞ ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞)) → -∞
< 𝑧) |
78 | | breq1 3982 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = -∞ → (𝑥 < 𝑧 ↔ -∞ < 𝑧)) |
79 | 78 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = -∞ ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞)) → (𝑥 < 𝑧 ↔ -∞ < 𝑧)) |
80 | 77, 79 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = -∞ ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞)) → 𝑥 < 𝑧) |
81 | 80 | orcd 723 |
. . . . . . . . . . . 12
⊢ ((𝑥 = -∞ ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞)) → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
82 | 81 | a1d 22 |
. . . . . . . . . . 11
⊢ ((𝑥 = -∞ ∧ (𝑧 ∈ ℝ ∨ 𝑧 = +∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
83 | | eqtr3 2184 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = -∞ ∧ 𝑧 = -∞) → 𝑥 = 𝑧) |
84 | 83 | breq1d 3989 |
. . . . . . . . . . . 12
⊢ ((𝑥 = -∞ ∧ 𝑧 = -∞) → (𝑥 < 𝑦 ↔ 𝑧 < 𝑦)) |
85 | | olc 701 |
. . . . . . . . . . . 12
⊢ (𝑧 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
86 | 84, 85 | syl6bi 162 |
. . . . . . . . . . 11
⊢ ((𝑥 = -∞ ∧ 𝑧 = -∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
87 | 82, 86 | jaodan 787 |
. . . . . . . . . 10
⊢ ((𝑥 = -∞ ∧ ((𝑧 ∈ ℝ ∨ 𝑧 = +∞) ∨ 𝑧 = -∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
88 | 75, 87 | sylan2b 285 |
. . . . . . . . 9
⊢ ((𝑥 = -∞ ∧ 𝑧 ∈ ℝ*)
→ (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
89 | 88 | ancoms 266 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ*
∧ 𝑥 = -∞) →
(𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
90 | 89 | adantlr 469 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = -∞) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
91 | 67, 73, 90 | 3jaodan 1295 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
92 | 91 | 3impa 1183 |
. . . . 5
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
93 | 7, 92 | syl3an3b 1265 |
. . . 4
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
94 | 93 | 3com13 1197 |
. . 3
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
95 | 94 | rgen3 2551 |
. 2
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* ∀𝑧 ∈ ℝ*
(𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)) |
96 | | df-iso 4272 |
. 2
⊢ ( < Or
ℝ* ↔ ( < Po ℝ* ∧ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* ∀𝑧 ∈ ℝ* (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))) |
97 | 6, 95, 96 | mpbir2an 931 |
1
⊢ < Or
ℝ* |