Step | Hyp | Ref
| Expression |
1 | | ltrelre 7831 |
. . . 4
⊢
<ℝ ⊆ (ℝ × ℝ) |
2 | 1 | brel 4678 |
. . 3
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ → (⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ)) |
3 | | opelreal 7825 |
. . . 4
⊢
(⟨𝐴,
0R⟩ ∈ ℝ ↔ 𝐴 ∈ R) |
4 | | opelreal 7825 |
. . . 4
⊢
(⟨𝐵,
0R⟩ ∈ ℝ ↔ 𝐵 ∈ R) |
5 | 3, 4 | anbi12i 460 |
. . 3
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) ↔ (𝐴 ∈
R ∧ 𝐵
∈ R)) |
6 | 2, 5 | sylib 122 |
. 2
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
7 | | ltrelsr 7736 |
. . 3
⊢
<R ⊆ (R ×
R) |
8 | 7 | brel 4678 |
. 2
⊢ (𝐴 <R
𝐵 → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
9 | | eleq1 2240 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(𝑥 ∈ ℝ ↔
⟨𝐴,
0R⟩ ∈ ℝ)) |
10 | 9 | anbi1d 465 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
((𝑥 ∈ ℝ ∧
𝑦 ∈ ℝ) ↔
(⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ))) |
11 | | eqeq1 2184 |
. . . . . . . . . . 11
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(𝑥 = ⟨𝑧,
0R⟩ ↔ ⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩)) |
12 | 11 | anbi1d 465 |
. . . . . . . . . 10
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
((𝑥 = ⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩))) |
13 | 12 | anbi1d 465 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(((𝑥 = ⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ ((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
14 | 13 | 2exbidv 1868 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
15 | 10, 14 | anbi12d 473 |
. . . . . . 7
⊢ (𝑥 = ⟨𝐴, 0R⟩ →
(((𝑥 ∈ ℝ ∧
𝑦 ∈ ℝ) ∧
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤)))) |
16 | | eleq1 2240 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(𝑦 ∈ ℝ ↔
⟨𝐵,
0R⟩ ∈ ℝ)) |
17 | 16 | anbi2d 464 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ))) |
18 | | eqeq1 2184 |
. . . . . . . . . . 11
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(𝑦 = ⟨𝑤,
0R⟩ ↔ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩)) |
19 | 18 | anbi2d 464 |
. . . . . . . . . 10
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ↔ (⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩))) |
20 | 19 | anbi1d 465 |
. . . . . . . . 9
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤))) |
21 | 20 | 2exbidv 1868 |
. . . . . . . 8
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))) |
22 | 17, 21 | anbi12d 473 |
. . . . . . 7
⊢ (𝑦 = ⟨𝐵, 0R⟩ →
(((⟨𝐴,
0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)))) |
23 | | df-lt 7823 |
. . . . . . 7
⊢
<ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))} |
24 | 15, 22, 23 | brabg 4269 |
. . . . . 6
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) → (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ((⟨𝐴, 0R⟩ ∈
ℝ ∧ ⟨𝐵,
0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)))) |
25 | 24 | bianabs 611 |
. . . . 5
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) → (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))) |
26 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
27 | 26 | eqresr 7834 |
. . . . . . . . . 10
⊢
(⟨𝑧,
0R⟩ = ⟨𝐴, 0R⟩ ↔
𝑧 = 𝐴) |
28 | | eqcom 2179 |
. . . . . . . . . 10
⊢
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ↔
⟨𝑧,
0R⟩ = ⟨𝐴,
0R⟩) |
29 | | eqcom 2179 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑧 ↔ 𝑧 = 𝐴) |
30 | 27, 28, 29 | 3bitr4i 212 |
. . . . . . . . 9
⊢
(⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ↔
𝐴 = 𝑧) |
31 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
32 | 31 | eqresr 7834 |
. . . . . . . . . 10
⊢
(⟨𝑤,
0R⟩ = ⟨𝐵, 0R⟩ ↔
𝑤 = 𝐵) |
33 | | eqcom 2179 |
. . . . . . . . . 10
⊢
(⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩ ↔
⟨𝑤,
0R⟩ = ⟨𝐵,
0R⟩) |
34 | | eqcom 2179 |
. . . . . . . . . 10
⊢ (𝐵 = 𝑤 ↔ 𝑤 = 𝐵) |
35 | 32, 33, 34 | 3bitr4i 212 |
. . . . . . . . 9
⊢
(⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩ ↔
𝐵 = 𝑤) |
36 | 30, 35 | anbi12i 460 |
. . . . . . . 8
⊢
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ↔
(𝐴 = 𝑧 ∧ 𝐵 = 𝑤)) |
37 | 26, 31 | opth2 4240 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝑤)) |
38 | 36, 37 | bitr4i 187 |
. . . . . . 7
⊢
((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ↔
⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩) |
39 | 38 | anbi1i 458 |
. . . . . 6
⊢
(((⟨𝐴,
0R⟩ = ⟨𝑧, 0R⟩ ∧
⟨𝐵,
0R⟩ = ⟨𝑤, 0R⟩) ∧
𝑧
<R 𝑤) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)) |
40 | 39 | 2exbii 1606 |
. . . . 5
⊢
(∃𝑧∃𝑤((⟨𝐴, 0R⟩ =
⟨𝑧,
0R⟩ ∧ ⟨𝐵, 0R⟩ =
⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)) |
41 | 25, 40 | bitrdi 196 |
. . . 4
⊢
((⟨𝐴,
0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈
ℝ) → (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))) |
42 | 3, 4, 41 | syl2anbr 292 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))) |
43 | | breq12 4008 |
. . . 4
⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → (𝑧 <R 𝑤 ↔ 𝐴 <R 𝐵)) |
44 | 43 | copsex2g 4246 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤) ↔ 𝐴 <R 𝐵)) |
45 | 42, 44 | bitrd 188 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ 𝐴 <R 𝐵)) |
46 | 6, 8, 45 | pm5.21nii 704 |
1
⊢
(⟨𝐴,
0R⟩ <ℝ ⟨𝐵,
0R⟩ ↔ 𝐴 <R 𝐵) |