Step | Hyp | Ref
| Expression |
1 | | ltrelre 11077 |
. . . 4
⊢
<ℝ ⊆ (ℝ × ℝ) |
2 | 1 | brel 5702 |
. . 3
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ → (⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ)) |
3 | | opelreal 11073 |
. . . 4
⊢
(⟨𝐴,
0R⟩ ∈ ℝ ↔ 𝐴 ∈ R) |
4 | | opelreal 11073 |
. . . 4
⊢
(⟨𝐵,
0R⟩ ∈ ℝ ↔ 𝐵 ∈ R) |
5 | 3, 4 | anbi12i 628 |
. . 3
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) ↔ (𝐴 ∈
R ∧ 𝐵
∈ R)) |
6 | 2, 5 | sylib 217 |
. 2
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
7 | | ltrelsr 11011 |
. . 3
⊢
<R ⊆ (R ×
R) |
8 | 7 | brel 5702 |
. 2
⊢ (𝐴 <R
𝐵 → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
9 | | opex 5426 |
. . . . . . 7
⊢
⟨𝐴,
0R⟩ ∈ V |
10 | | opex 5426 |
. . . . . . 7
⊢
⟨𝐵,
0R⟩ ∈ V |
11 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(𝑥 ∈ ℝ ↔
⟨𝐴,
0R⟩ ∈ ℝ)) |
12 | 11 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
((𝑥 ∈ ℝ ∧
𝑦 ∈ ℝ) ↔
(⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ))) |
13 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(𝑥 = ⟨𝑧,
0R⟩ ↔ ⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩)) |
14 | 13 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
((𝑥 = ⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩))) |
15 | 14 | anbi1d 631 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(((𝑥 = ⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ ((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
16 | 15 | 2exbidv 1928 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
17 | 12, 16 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(((𝑥 ∈ ℝ ∧
𝑦 ∈ ℝ) ∧
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤)))) |
18 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(𝑦 ∈ ℝ ↔
⟨𝐵,
0R⟩ ∈ ℝ)) |
19 | 18 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ))) |
20 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(𝑦 = ⟨𝑤,
0R⟩ ↔ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩)) |
21 | 20 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ↔ (⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩))) |
22 | 21 | anbi1d 631 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
23 | 22 | 2exbidv 1928 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))) |
24 | 19, 23 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)))) |
25 | | df-lt 11071 |
. . . . . . 7
⊢
<ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))} |
26 | 9, 10, 17, 24, 25 | brab 5505 |
. . . . . 6
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ((⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))) |
27 | 26 | baib 537 |
. . . . 5
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) → (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))) |
28 | | vex 3452 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
29 | 28 | eqresr 11080 |
. . . . . . . . . 10
⊢
(⟨𝑧,
0R⟩ = ⟨𝐴, 0R⟩ ↔
𝑧 = 𝐴) |
30 | | eqcom 2744 |
. . . . . . . . . 10
⊢
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ↔
⟨𝑧,
0R⟩ = ⟨𝐴,
0R⟩) |
31 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑧 ↔ 𝑧 = 𝐴) |
32 | 29, 30, 31 | 3bitr4i 303 |
. . . . . . . . 9
⊢
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ↔
𝐴 = 𝑧) |
33 | | vex 3452 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
34 | 33 | eqresr 11080 |
. . . . . . . . . 10
⊢
(⟨𝑤,
0R⟩ = ⟨𝐵, 0R⟩ ↔
𝑤 = 𝐵) |
35 | | eqcom 2744 |
. . . . . . . . . 10
⊢
(⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩ ↔
⟨𝑤,
0R⟩ = ⟨𝐵,
0R⟩) |
36 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝐵 = 𝑤 ↔ 𝑤 = 𝐵) |
37 | 34, 35, 36 | 3bitr4i 303 |
. . . . . . . . 9
⊢
(⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩ ↔
𝐵 = 𝑤) |
38 | 32, 37 | anbi12i 628 |
. . . . . . . 8
⊢
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ↔
(𝐴 = 𝑧 ∧ 𝐵 = 𝑤)) |
39 | 28, 33 | opth2 5442 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝑤)) |
40 | 38, 39 | bitr4i 278 |
. . . . . . 7
⊢
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ↔
⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩) |
41 | 40 | anbi1i 625 |
. . . . . 6
⊢
(((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)) |
42 | 41 | 2exbii 1852 |
. . . . 5
⊢
(∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)) |
43 | 27, 42 | bitrdi 287 |
. . . 4
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) → (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))) |
44 | 3, 4, 43 | syl2anbr 600 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))) |
45 | | breq12 5115 |
. . . 4
⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → (𝑧 <R 𝑤 ↔ 𝐴 <R 𝐵)) |
46 | 45 | copsex2g 5455 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤) ↔ 𝐴 <R 𝐵)) |
47 | 44, 46 | bitrd 279 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ 𝐴 <R 𝐵)) |
48 | 6, 8, 47 | pm5.21nii 380 |
1
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ 𝐴 <R 𝐵) |