Description: Implication of eqvreldisj3 , lemma for the Member Partition Equivalence Theorem mpet3 . (Contributed by Peter Mazsa, 27-Oct-2020) (Revised by Peter Mazsa, 24-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eqvrelqseqdisj3 | ⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( ◡ E ↾ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqvreldisj3 | ⊢ ( EqvRel 𝑅 → Disj ( ◡ E ↾ ( 𝐵 / 𝑅 ) ) ) | |
| 2 | 1 | adantr | ⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( ◡ E ↾ ( 𝐵 / 𝑅 ) ) ) |
| 3 | reseq2 | ⊢ ( ( 𝐵 / 𝑅 ) = 𝐴 → ( ◡ E ↾ ( 𝐵 / 𝑅 ) ) = ( ◡ E ↾ 𝐴 ) ) | |
| 4 | 3 | disjeqd | ⊢ ( ( 𝐵 / 𝑅 ) = 𝐴 → ( Disj ( ◡ E ↾ ( 𝐵 / 𝑅 ) ) ↔ Disj ( ◡ E ↾ 𝐴 ) ) ) |
| 5 | 4 | adantl | ⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → ( Disj ( ◡ E ↾ ( 𝐵 / 𝑅 ) ) ↔ Disj ( ◡ E ↾ 𝐴 ) ) ) |
| 6 | 2 5 | mpbid | ⊢ ( ( EqvRel 𝑅 ∧ ( 𝐵 / 𝑅 ) = 𝐴 ) → Disj ( ◡ E ↾ 𝐴 ) ) |