Step | Hyp | Ref
| Expression |
1 | | lerel 10504 |
. . 3
⊢ Rel
≤ |
2 | | lerelxr 10503 |
. . . . . . . . . . 11
⊢ ≤
⊆ (ℝ* × ℝ*) |
3 | 2 | brel 5464 |
. . . . . . . . . 10
⊢ (𝑥 ≤ 𝑦 → (𝑥 ∈ ℝ* ∧ 𝑦 ∈
ℝ*)) |
4 | 3 | adantr 473 |
. . . . . . . . 9
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → (𝑥 ∈ ℝ* ∧ 𝑦 ∈
ℝ*)) |
5 | 4 | simpld 487 |
. . . . . . . 8
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ∈ ℝ*) |
6 | 4 | simprd 488 |
. . . . . . . 8
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑦 ∈ ℝ*) |
7 | 2 | brel 5464 |
. . . . . . . . . 10
⊢ (𝑦 ≤ 𝑧 → (𝑦 ∈ ℝ* ∧ 𝑧 ∈
ℝ*)) |
8 | 7 | simprd 488 |
. . . . . . . . 9
⊢ (𝑦 ≤ 𝑧 → 𝑧 ∈ ℝ*) |
9 | 8 | adantl 474 |
. . . . . . . 8
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑧 ∈ ℝ*) |
10 | 5, 6, 9 | 3jca 1109 |
. . . . . . 7
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ*)) |
11 | | xrletr 12367 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
12 | 10, 11 | mpcom 38 |
. . . . . 6
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) |
13 | 12 | ax-gen 1759 |
. . . . 5
⊢
∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) |
14 | 13 | gen2 1760 |
. . . 4
⊢
∀𝑥∀𝑦∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) |
15 | | cotr 5810 |
. . . 4
⊢ (( ≤
∘ ≤ ) ⊆ ≤ ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
16 | 14, 15 | mpbir 223 |
. . 3
⊢ ( ≤
∘ ≤ ) ⊆ ≤ |
17 | | asymref 5814 |
. . . 4
⊢ (( ≤
∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) ↔ ∀𝑥 ∈ ∪ ∪ ≤ ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
18 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) |
19 | 2 | brel 5464 |
. . . . . . . . . . . 12
⊢ (𝑦 ≤ 𝑥 → (𝑦 ∈ ℝ* ∧ 𝑥 ∈
ℝ*)) |
20 | 19 | simpld 487 |
. . . . . . . . . . 11
⊢ (𝑦 ≤ 𝑥 → 𝑦 ∈ ℝ*) |
21 | 20 | adantl 474 |
. . . . . . . . . 10
⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑦 ∈ ℝ*) |
22 | | xrletri3 12363 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))) |
23 | 21, 22 | sylan2 584 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))) |
24 | 18, 23 | mpbird 249 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 = 𝑦) |
25 | 24 | ex 405 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ*
→ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
26 | | xrleid 12360 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ 𝑥 ≤ 𝑥) |
27 | 26, 26 | jca 504 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ (𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥)) |
28 | | breq2 4930 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑥 ↔ 𝑥 ≤ 𝑦)) |
29 | | breq1 4929 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑥 ↔ 𝑦 ≤ 𝑥)) |
30 | 28, 29 | anbi12d 622 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥) ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))) |
31 | 27, 30 | syl5ibcom 237 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ*
→ (𝑥 = 𝑦 → (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))) |
32 | 25, 31 | impbid 204 |
. . . . . 6
⊢ (𝑥 ∈ ℝ*
→ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
33 | 32 | alrimiv 1887 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
34 | | lefld 17707 |
. . . . . 6
⊢
ℝ* = ∪ ∪ ≤ |
35 | 34 | eqcomi 2782 |
. . . . 5
⊢ ∪ ∪ ≤ =
ℝ* |
36 | 33, 35 | eleq2s 2879 |
. . . 4
⊢ (𝑥 ∈ ∪ ∪ ≤ → ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
37 | 17, 36 | mprgbir 3098 |
. . 3
⊢ ( ≤
∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) |
38 | | xrex 12200 |
. . . . . 6
⊢
ℝ* ∈ V |
39 | 38, 38 | xpex 7292 |
. . . . 5
⊢
(ℝ* × ℝ*) ∈
V |
40 | 39, 2 | ssexi 5079 |
. . . 4
⊢ ≤
∈ V |
41 | | isps 17683 |
. . . 4
⊢ ( ≤
∈ V → ( ≤ ∈ PosetRel ↔ (Rel ≤ ∧ ( ≤ ∘
≤ ) ⊆ ≤ ∧ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ )))) |
42 | 40, 41 | ax-mp 5 |
. . 3
⊢ ( ≤
∈ PosetRel ↔ (Rel ≤ ∧ ( ≤ ∘ ≤ ) ⊆ ≤ ∧
( ≤ ∩ ◡ ≤ ) = ( I ↾
∪ ∪ ≤
))) |
43 | 1, 16, 37, 42 | mpbir3an 1322 |
. 2
⊢ ≤
∈ PosetRel |
44 | | xrletri 12362 |
. . . 4
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
45 | 44 | rgen2a 3171 |
. . 3
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) |
46 | | qfto 5819 |
. . 3
⊢
((ℝ* × ℝ*) ⊆ ( ≤ ∪
◡ ≤ ) ↔ ∀𝑥 ∈ ℝ*
∀𝑦 ∈
ℝ* (𝑥 ≤
𝑦 ∨ 𝑦 ≤ 𝑥)) |
47 | 45, 46 | mpbir 223 |
. 2
⊢
(ℝ* × ℝ*) ⊆ ( ≤ ∪
◡ ≤ ) |
48 | | ledm 17705 |
. . 3
⊢
ℝ* = dom ≤ |
49 | 48 | istsr 17698 |
. 2
⊢ ( ≤
∈ TosetRel ↔ ( ≤ ∈ PosetRel ∧ (ℝ*
× ℝ*) ⊆ ( ≤ ∪ ◡ ≤ ))) |
50 | 43, 47, 49 | mpbir2an 699 |
1
⊢ ≤
∈ TosetRel |