Metamath Proof Explorer

Theorem petincnvepres2

Description: A partition-equivalence theorem with intersection and general R . (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion petincnvepres2 ⊢ Disj R ∩ E -1 ↾ A ∧ dom ⁡ R ∩ E -1 ↾ A / R ∩ E -1 ↾ A = A ↔ EqvRel ≀ R ∩ E -1 ↾ A ∧ dom ⁡ ≀ R ∩ E -1 ↾ A / ≀ R ∩ E -1 ↾ A = A

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj4 ⊢ EqvRel ≀ R ∩ E -1 ↾ A ∧ dom ⁡ ≀ R ∩ E -1 ↾ A / ≀ R ∩ E -1 ↾ A = A → Disj R ∩ E -1 ↾ A
2 1 petlem ⊢ Disj R ∩ E -1 ↾ A ∧ dom ⁡ R ∩ E -1 ↾ A / R ∩ E -1 ↾ A = A ↔ EqvRel ≀ R ∩ E -1 ↾ A ∧ dom ⁡ ≀ R ∩ E -1 ↾ A / ≀ R ∩ E -1 ↾ A = A