Step | Hyp | Ref
| Expression |
1 | | brecop2.3 |
. . . 4
⊢ 𝑅 ⊆ (𝐻 × 𝐻) |
2 | 1 | brel 5698 |
. . 3
⊢
([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ →
([⟨𝐴, 𝐵⟩] ∼ ∈ 𝐻 ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ 𝐻)) |
3 | | brecop2.1 |
. . . . . . 7
⊢ dom ∼ =
(𝐺 × 𝐺) |
4 | | ecelqsdm 8727 |
. . . . . . 7
⊢ ((dom
∼
= (𝐺 × 𝐺) ∧ [⟨𝐴, 𝐵⟩] ∼ ∈ ((𝐺 × 𝐺) / ∼ )) →
⟨𝐴, 𝐵⟩ ∈ (𝐺 × 𝐺)) |
5 | 3, 4 | mpan 689 |
. . . . . 6
⊢
([⟨𝐴, 𝐵⟩] ∼ ∈ ((𝐺 × 𝐺) / ∼ ) →
⟨𝐴, 𝐵⟩ ∈ (𝐺 × 𝐺)) |
6 | | brecop2.2 |
. . . . . 6
⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) |
7 | 5, 6 | eleq2s 2856 |
. . . . 5
⊢
([⟨𝐴, 𝐵⟩] ∼ ∈ 𝐻 → ⟨𝐴, 𝐵⟩ ∈ (𝐺 × 𝐺)) |
8 | | opelxp 5670 |
. . . . 5
⊢
(⟨𝐴, 𝐵⟩ ∈ (𝐺 × 𝐺) ↔ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) |
9 | 7, 8 | sylib 217 |
. . . 4
⊢
([⟨𝐴, 𝐵⟩] ∼ ∈ 𝐻 → (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) |
10 | | ecelqsdm 8727 |
. . . . . . 7
⊢ ((dom
∼
= (𝐺 × 𝐺) ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ ((𝐺 × 𝐺) / ∼ )) →
⟨𝐶, 𝐷⟩ ∈ (𝐺 × 𝐺)) |
11 | 3, 10 | mpan 689 |
. . . . . 6
⊢
([⟨𝐶, 𝐷⟩] ∼ ∈ ((𝐺 × 𝐺) / ∼ ) →
⟨𝐶, 𝐷⟩ ∈ (𝐺 × 𝐺)) |
12 | 11, 6 | eleq2s 2856 |
. . . . 5
⊢
([⟨𝐶, 𝐷⟩] ∼ ∈ 𝐻 → ⟨𝐶, 𝐷⟩ ∈ (𝐺 × 𝐺)) |
13 | | opelxp 5670 |
. . . . 5
⊢
(⟨𝐶, 𝐷⟩ ∈ (𝐺 × 𝐺) ↔ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) |
14 | 12, 13 | sylib 217 |
. . . 4
⊢
([⟨𝐶, 𝐷⟩] ∼ ∈ 𝐻 → (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) |
15 | 9, 14 | anim12i 614 |
. . 3
⊢
(([⟨𝐴, 𝐵⟩] ∼ ∈ 𝐻 ∧ [⟨𝐶, 𝐷⟩] ∼ ∈ 𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) |
16 | 2, 15 | syl 17 |
. 2
⊢
([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) |
17 | | brecop2.4 |
. . . . 5
⊢ ≤ ⊆
(𝐺 × 𝐺) |
18 | 17 | brel 5698 |
. . . 4
⊢ ((𝐴 + 𝐷) ≤ (𝐵 + 𝐶) → ((𝐴 + 𝐷) ∈ 𝐺 ∧ (𝐵 + 𝐶) ∈ 𝐺)) |
19 | | brecop2.6 |
. . . . . 6
⊢ dom + = (𝐺 × 𝐺) |
20 | | brecop2.5 |
. . . . . 6
⊢ ¬
∅ ∈ 𝐺 |
21 | 19, 20 | ndmovrcl 7541 |
. . . . 5
⊢ ((𝐴 + 𝐷) ∈ 𝐺 → (𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) |
22 | 19, 20 | ndmovrcl 7541 |
. . . . 5
⊢ ((𝐵 + 𝐶) ∈ 𝐺 → (𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺)) |
23 | 21, 22 | anim12i 614 |
. . . 4
⊢ (((𝐴 + 𝐷) ∈ 𝐺 ∧ (𝐵 + 𝐶) ∈ 𝐺) → ((𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺) ∧ (𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺))) |
24 | 18, 23 | syl 17 |
. . 3
⊢ ((𝐴 + 𝐷) ≤ (𝐵 + 𝐶) → ((𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺) ∧ (𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺))) |
25 | | an42 656 |
. . 3
⊢ (((𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺) ∧ (𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺)) ↔ ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) |
26 | 24, 25 | sylib 217 |
. 2
⊢ ((𝐴 + 𝐷) ≤ (𝐵 + 𝐶) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) |
27 | | brecop2.7 |
. 2
⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶))) |
28 | 16, 26, 27 | pm5.21nii 380 |
1
⊢
([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶)) |