| Step | Hyp | Ref
| Expression |
| 1 | | ltrelre 11174 |
. . . 4
⊢
<ℝ ⊆ (ℝ × ℝ) |
| 2 | 1 | brel 5750 |
. . 3
⊢
(〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 → (〈𝐴, 0R〉 ∈
ℝ ∧ 〈𝐵,
0R〉 ∈ ℝ)) |
| 3 | | opelreal 11170 |
. . . 4
⊢
(〈𝐴,
0R〉 ∈ ℝ ↔ 𝐴 ∈ R) |
| 4 | | opelreal 11170 |
. . . 4
⊢
(〈𝐵,
0R〉 ∈ ℝ ↔ 𝐵 ∈ R) |
| 5 | 3, 4 | anbi12i 628 |
. . 3
⊢
((〈𝐴,
0R〉 ∈ ℝ ∧ 〈𝐵, 0R〉 ∈
ℝ) ↔ (𝐴 ∈
R ∧ 𝐵
∈ R)) |
| 6 | 2, 5 | sylib 218 |
. 2
⊢
(〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
| 7 | | ltrelsr 11108 |
. . 3
⊢
<R ⊆ (R ×
R) |
| 8 | 7 | brel 5750 |
. 2
⊢ (𝐴 <R
𝐵 → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
| 9 | | opex 5469 |
. . . . . . 7
⊢
〈𝐴,
0R〉 ∈ V |
| 10 | | opex 5469 |
. . . . . . 7
⊢
〈𝐵,
0R〉 ∈ V |
| 11 | | eleq1 2829 |
. . . . . . . . 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 1924 |
. . . . . . . 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 2829 |
. . . . . . . . 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 1924 |
. . . . . . . 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 11168 |
. . . . . . 7
⊢
<ℝ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) ∧ 𝑧 <R 𝑤))} |
| 26 | 9, 10, 17, 24, 25 | brab 5548 |
. . . . . 6
⊢
(〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ ((〈𝐴, 0R〉 ∈
ℝ ∧ 〈𝐵,
0R〉 ∈ ℝ) ∧ ∃𝑧∃𝑤((〈𝐴, 0R〉 =
〈𝑧,
0R〉 ∧ 〈𝐵, 0R〉 =
〈𝑤,
0R〉) ∧ 𝑧 <R 𝑤))) |
| 27 | 26 | baib 535 |
. . . . 5
⊢
((〈𝐴,
0R〉 ∈ ℝ ∧ 〈𝐵, 0R〉 ∈
ℝ) → (〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ ∃𝑧∃𝑤((〈𝐴, 0R〉 =
〈𝑧,
0R〉 ∧ 〈𝐵, 0R〉 =
〈𝑤,
0R〉) ∧ 𝑧 <R 𝑤))) |
| 28 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 29 | 28 | eqresr 11177 |
. . . . . . . . . 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 3484 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
| 34 | 33 | eqresr 11177 |
. . . . . . . . . 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 5485 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝑤)) |
| 40 | 38, 39 | bitr4i 278 |
. . . . . . 7
⊢
((〈𝐴,
0R〉 = 〈𝑧, 0R〉 ∧
〈𝐵,
0R〉 = 〈𝑤, 0R〉) ↔
〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉) |
| 41 | 40 | anbi1i 624 |
. . . . . 6
⊢
(((〈𝐴,
0R〉 = 〈𝑧, 0R〉 ∧
〈𝐵,
0R〉 = 〈𝑤, 0R〉) ∧
𝑧
<R 𝑤) ↔ (〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑧 <R 𝑤)) |
| 42 | 41 | 2exbii 1849 |
. . . . 5
⊢
(∃𝑧∃𝑤((〈𝐴, 0R〉 =
〈𝑧,
0R〉 ∧ 〈𝐵, 0R〉 =
〈𝑤,
0R〉) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤(〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑧 <R 𝑤)) |
| 43 | 27, 42 | bitrdi 287 |
. . . 4
⊢
((〈𝐴,
0R〉 ∈ ℝ ∧ 〈𝐵, 0R〉 ∈
ℝ) → (〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ ∃𝑧∃𝑤(〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑧 <R 𝑤))) |
| 44 | 3, 4, 43 | syl2anbr 599 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ ∃𝑧∃𝑤(〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑧 <R 𝑤))) |
| 45 | | breq12 5148 |
. . . 4
⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → (𝑧 <R 𝑤 ↔ 𝐴 <R 𝐵)) |
| 46 | 45 | copsex2g 5498 |
. . 3
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (∃𝑧∃𝑤(〈𝐴, 𝐵〉 = 〈𝑧, 𝑤〉 ∧ 𝑧 <R 𝑤) ↔ 𝐴 <R 𝐵)) |
| 47 | 44, 46 | bitrd 279 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ 𝐴 <R 𝐵)) |
| 48 | 6, 8, 47 | pm5.21nii 378 |
1
⊢
(〈𝐴,
0R〉 <ℝ 〈𝐵,
0R〉 ↔ 𝐴 <R 𝐵) |