Step | Hyp | Ref
| Expression |
1 | | ltrelre 6730 |
. . . 4
⊢
<ℝ ⊆ (ℝ × ℝ) |
2 | 1 | brel 4335 |
. . 3
⊢
(〈A,
0R〉 <ℝ 〈B, 0R〉 →
(〈A, 0R〉
∈ ℝ ∧
〈B, 0R〉
∈ ℝ)) |
3 | | opelreal 6726 |
. . . 4
⊢
(〈A,
0R〉 ∈ ℝ
↔ A ∈ R) |
4 | | opelreal 6726 |
. . . 4
⊢
(〈B,
0R〉 ∈ ℝ
↔ B ∈ R) |
5 | 3, 4 | anbi12i 433 |
. . 3
⊢
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
↔ (A ∈ R ∧ B ∈ R)) |
6 | 2, 5 | sylib 127 |
. 2
⊢
(〈A,
0R〉 <ℝ 〈B, 0R〉 →
(A ∈
R ∧ B ∈
R)) |
7 | | ltrelsr 6666 |
. . 3
⊢
<R ⊆ (R ×
R) |
8 | 7 | brel 4335 |
. 2
⊢ (A <R B → (A
∈ R ∧ B ∈ R)) |
9 | | eleq1 2097 |
. . . . . . . . 9
⊢ (x = 〈A,
0R〉 → (x
∈ ℝ ↔ 〈A, 0R〉 ∈ ℝ)) |
10 | 9 | anbi1d 438 |
. . . . . . . 8
⊢ (x = 〈A,
0R〉 → ((x ∈ ℝ ∧ y ∈ ℝ) ↔ (〈A, 0R〉 ∈ ℝ ∧
y ∈
ℝ))) |
11 | | eqeq1 2043 |
. . . . . . . . . . 11
⊢ (x = 〈A,
0R〉 → (x
= 〈z,
0R〉 ↔ 〈A, 0R〉 =
〈z,
0R〉)) |
12 | 11 | anbi1d 438 |
. . . . . . . . . 10
⊢ (x = 〈A,
0R〉 → ((x = 〈z,
0R〉 ∧ y = 〈w,
0R〉) ↔ (〈A, 0R〉 =
〈z, 0R〉
∧ y =
〈w,
0R〉))) |
13 | 12 | anbi1d 438 |
. . . . . . . . 9
⊢ (x = 〈A,
0R〉 → (((x = 〈z,
0R〉 ∧ y = 〈w,
0R〉) ∧ z <R w) ↔ ((〈A, 0R〉 =
〈z, 0R〉
∧ y =
〈w, 0R〉)
∧ z
<R w))) |
14 | 13 | 2exbidv 1745 |
. . . . . . . 8
⊢ (x = 〈A,
0R〉 → (∃z∃w((x = 〈z,
0R〉 ∧ y = 〈w,
0R〉) ∧ z <R w) ↔ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ y =
〈w, 0R〉)
∧ z
<R w))) |
15 | 10, 14 | anbi12d 442 |
. . . . . . 7
⊢ (x = 〈A,
0R〉 → (((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = 〈z,
0R〉 ∧ y = 〈w,
0R〉) ∧ z <R w)) ↔ ((〈A, 0R〉 ∈ ℝ ∧
y ∈
ℝ) ∧ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ y =
〈w, 0R〉)
∧ z
<R w)))) |
16 | | eleq1 2097 |
. . . . . . . . 9
⊢ (y = 〈B,
0R〉 → (y
∈ ℝ ↔ 〈B, 0R〉 ∈ ℝ)) |
17 | 16 | anbi2d 437 |
. . . . . . . 8
⊢ (y = 〈B,
0R〉 → ((〈A, 0R〉 ∈ ℝ ∧
y ∈
ℝ) ↔ (〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈
ℝ))) |
18 | | eqeq1 2043 |
. . . . . . . . . . 11
⊢ (y = 〈B,
0R〉 → (y
= 〈w,
0R〉 ↔ 〈B, 0R〉 =
〈w,
0R〉)) |
19 | 18 | anbi2d 437 |
. . . . . . . . . 10
⊢ (y = 〈B,
0R〉 → ((〈A, 0R〉 =
〈z, 0R〉
∧ y =
〈w, 0R〉)
↔ (〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w,
0R〉))) |
20 | 19 | anbi1d 438 |
. . . . . . . . 9
⊢ (y = 〈B,
0R〉 → (((〈A, 0R〉 =
〈z, 0R〉
∧ y =
〈w, 0R〉)
∧ z
<R w) ↔
((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w))) |
21 | 20 | 2exbidv 1745 |
. . . . . . . 8
⊢ (y = 〈B,
0R〉 → (∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ y =
〈w, 0R〉)
∧ z
<R w) ↔
∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w))) |
22 | 17, 21 | anbi12d 442 |
. . . . . . 7
⊢ (y = 〈B,
0R〉 → (((〈A, 0R〉 ∈ ℝ ∧
y ∈
ℝ) ∧ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ y =
〈w, 0R〉)
∧ z
<R w)) ↔
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
∧ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w)))) |
23 | | df-lt 6724 |
. . . . . . 7
⊢
<ℝ = {〈x, y〉 ∣ ((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = 〈z,
0R〉 ∧ y = 〈w,
0R〉) ∧ z <R w))} |
24 | 15, 22, 23 | brabg 3997 |
. . . . . 6
⊢
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
→ (〈A,
0R〉 <ℝ 〈B, 0R〉 ↔
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
∧ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w)))) |
25 | 24 | bianabs 543 |
. . . . 5
⊢
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
→ (〈A,
0R〉 <ℝ 〈B, 0R〉 ↔ ∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w))) |
26 | | vex 2554 |
. . . . . . . . . . 11
⊢ z ∈
V |
27 | 26 | eqresr 6733 |
. . . . . . . . . 10
⊢
(〈z,
0R〉 = 〈A, 0R〉 ↔ z = A) |
28 | | eqcom 2039 |
. . . . . . . . . 10
⊢
(〈A,
0R〉 = 〈z, 0R〉 ↔
〈z, 0R〉
= 〈A,
0R〉) |
29 | | eqcom 2039 |
. . . . . . . . . 10
⊢ (A = z ↔
z = A) |
30 | 27, 28, 29 | 3bitr4i 201 |
. . . . . . . . 9
⊢
(〈A,
0R〉 = 〈z, 0R〉 ↔ A = z) |
31 | | vex 2554 |
. . . . . . . . . . 11
⊢ w ∈
V |
32 | 31 | eqresr 6733 |
. . . . . . . . . 10
⊢
(〈w,
0R〉 = 〈B, 0R〉 ↔ w = B) |
33 | | eqcom 2039 |
. . . . . . . . . 10
⊢
(〈B,
0R〉 = 〈w, 0R〉 ↔
〈w, 0R〉
= 〈B,
0R〉) |
34 | | eqcom 2039 |
. . . . . . . . . 10
⊢ (B = w ↔
w = B) |
35 | 32, 33, 34 | 3bitr4i 201 |
. . . . . . . . 9
⊢
(〈B,
0R〉 = 〈w, 0R〉 ↔ B = w) |
36 | 30, 35 | anbi12i 433 |
. . . . . . . 8
⊢
((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ↔
(A = z
∧ B =
w)) |
37 | 26, 31 | opth2 3968 |
. . . . . . . 8
⊢
(〈A, B〉 = 〈z, w〉
↔ (A = z ∧ B = w)) |
38 | 36, 37 | bitr4i 176 |
. . . . . . 7
⊢
((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ↔
〈A, B〉 = 〈z, w〉) |
39 | 38 | anbi1i 431 |
. . . . . 6
⊢
(((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w) ↔
(〈A, B〉 = 〈z, w〉 ∧ z
<R w)) |
40 | 39 | 2exbii 1494 |
. . . . 5
⊢ (∃z∃w((〈A,
0R〉 = 〈z, 0R〉 ∧ 〈B,
0R〉 = 〈w, 0R〉) ∧ z
<R w) ↔
∃z∃w(〈A,
B〉 = 〈z, w〉 ∧ z
<R w)) |
41 | 25, 40 | syl6bb 185 |
. . . 4
⊢
((〈A,
0R〉 ∈ ℝ
∧ 〈B,
0R〉 ∈ ℝ)
→ (〈A,
0R〉 <ℝ 〈B, 0R〉 ↔ ∃z∃w(〈A,
B〉 = 〈z, w〉 ∧ z
<R w))) |
42 | 3, 4, 41 | syl2anbr 276 |
. . 3
⊢
((A ∈ R ∧ B ∈ R) → (〈A, 0R〉
<ℝ 〈B,
0R〉 ↔ ∃z∃w(〈A,
B〉 = 〈z, w〉 ∧ z
<R w))) |
43 | | breq12 3760 |
. . . 4
⊢
((z = A ∧ w = B) →
(z <R w ↔ A
<R B)) |
44 | 43 | copsex2g 3974 |
. . 3
⊢
((A ∈ R ∧ B ∈ R) → (∃z∃w(〈A,
B〉 = 〈z, w〉 ∧ z
<R w) ↔
A <R B)) |
45 | 42, 44 | bitrd 177 |
. 2
⊢
((A ∈ R ∧ B ∈ R) → (〈A, 0R〉
<ℝ 〈B,
0R〉 ↔ A
<R B)) |
46 | 6, 8, 45 | pm5.21nii 619 |
1
⊢
(〈A,
0R〉 <ℝ 〈B, 0R〉 ↔ A <R B) |