Step | Hyp | Ref
| Expression |
1 | | breq 3967 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑥 ↔ 𝑥𝑆𝑥)) |
2 | 1 | notbid 657 |
. . . . 5
⊢ (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑥𝑆𝑥)) |
3 | | breq 3967 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
4 | | breq 3967 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
5 | 3, 4 | anbi12d 465 |
. . . . . 6
⊢ (𝑅 = 𝑆 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧))) |
6 | | breq 3967 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑧 ↔ 𝑥𝑆𝑧)) |
7 | 5, 6 | imbi12d 233 |
. . . . 5
⊢ (𝑅 = 𝑆 → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑆𝑧))) |
8 | 2, 7 | anbi12d 465 |
. . . 4
⊢ (𝑅 = 𝑆 → ((¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑆𝑥 ∧ ((𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑆𝑧)))) |
9 | 8 | ralbidv 2457 |
. . 3
⊢ (𝑅 = 𝑆 → (∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑆𝑥 ∧ ((𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑆𝑧)))) |
10 | 9 | 2ralbidv 2481 |
. 2
⊢ (𝑅 = 𝑆 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑆𝑥 ∧ ((𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑆𝑧)))) |
11 | | df-po 4256 |
. 2
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
12 | | df-po 4256 |
. 2
⊢ (𝑆 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑆𝑥 ∧ ((𝑥𝑆𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑆𝑧))) |
13 | 10, 11, 12 | 3bitr4g 222 |
1
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) |