Proof of Theorem sotri
Step | Hyp | Ref
| Expression |
1 | | soi.2 |
. . . . 5
⊢ 𝑅 ⊆ (𝑆 × 𝑆) |
2 | 1 | brel 4392 |
. . . 4
⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
3 | 2 | simpld 105 |
. . 3
⊢ (𝐴𝑅𝐵 → 𝐴 ∈ 𝑆) |
4 | 1 | brel 4392 |
. . 3
⊢ (𝐵𝑅𝐶 → (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) |
5 | 3, 4 | anim12i 321 |
. 2
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) |
6 | | soi.1 |
. . . 4
⊢ 𝑅 Or 𝑆 |
7 | | sotr 4055 |
. . . 4
⊢ ((𝑅 Or 𝑆 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
8 | 6, 7 | mpan 400 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
9 | 8 | 3expb 1105 |
. 2
⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
10 | 5, 9 | mpcom 32 |
1
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |