Step | Hyp | Ref
| Expression |
1 | | issod.1 |
. 2
⊢ (𝜑 → 𝑅 Po 𝐴) |
2 | | issod.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
3 | 2 | 3adant3 1012 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
4 | | orc 707 |
. . . . . . . . . . . 12
⊢ (𝑥𝑅𝑦 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)) |
5 | 4 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
6 | | simp3r 1021 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → 𝑥𝑅𝑧) |
7 | | breq1 3992 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑧 ↔ 𝑦𝑅𝑧)) |
8 | 6, 7 | syl5ibcom 154 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥 = 𝑦 → 𝑦𝑅𝑧)) |
9 | | olc 706 |
. . . . . . . . . . . 12
⊢ (𝑦𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)) |
10 | 8, 9 | syl6 33 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥 = 𝑦 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
11 | | simp1 992 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → 𝜑) |
12 | | simp2r 1019 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → 𝑦 ∈ 𝐴) |
13 | | simp2l 1018 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → 𝑥 ∈ 𝐴) |
14 | | simp3l 1020 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → 𝑧 ∈ 𝐴) |
15 | 12, 13, 14 | 3jca 1172 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) |
16 | | potr 4293 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑦𝑅𝑥 ∧ 𝑥𝑅𝑧) → 𝑦𝑅𝑧)) |
17 | 1, 16 | sylan 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑦𝑅𝑥 ∧ 𝑥𝑅𝑧) → 𝑦𝑅𝑧)) |
18 | 17 | expcomd 1434 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑧 → (𝑦𝑅𝑥 → 𝑦𝑅𝑧))) |
19 | 18 | imp 123 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑥𝑅𝑧) → (𝑦𝑅𝑥 → 𝑦𝑅𝑧)) |
20 | 11, 15, 6, 19 | syl21anc 1232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑦𝑅𝑥 → 𝑦𝑅𝑧)) |
21 | 20, 9 | syl6 33 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑦𝑅𝑥 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
22 | 5, 10, 21 | 3jaod 1299 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
23 | 3, 22 | mpd 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)) |
24 | 23 | 3expa 1198 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥𝑅𝑧)) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)) |
25 | 24 | expr 373 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) → (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
26 | 25 | ralrimiva 2543 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
27 | 26 | anassrs 398 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
28 | 27 | ralrimiva 2543 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
29 | | ralcom 2633 |
. . . 4
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
30 | 28, 29 | sylib 121 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
31 | 30 | ralrimiva 2543 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧))) |
32 | | df-iso 4282 |
. 2
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑧 → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑧)))) |
33 | 1, 31, 32 | sylanbrc 415 |
1
⊢ (𝜑 → 𝑅 Or 𝐴) |