This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Lemma for the Partition-Equivalence Theorem pet2 . (Contributed by Peter Mazsa, 15-Jul-2020) (Revised by Peter Mazsa, 22-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
eqvrelqseqdisj5 |
⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( 𝑆 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqvrelqseqdisj3 |
⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( ◡ E ↾ 𝐴 ) ) |
| 2 |
|
disjimxrn |
⊢ ( Disj ( ◡ E ↾ 𝐴 ) → Disj ( 𝑆 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
| 3 |
1 2
|
syl |
⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( 𝑆 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |