This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem petincnvepres

Description: The shortest form of a partition-equivalence theorem with intersection and general R . Cf. br1cossincnvepres . Cf. pet . (Contributed by Peter Mazsa, 23-Sep-2021)

Ref Expression
Assertion petincnvepres ⊢ R ∩ E -1 ↾ A Part A ↔ ≀ R ∩ E -1 ↾ A ErALTV A

Proof

Step Hyp Ref Expression
1 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
2 dfpart2 ⊢ R ∩ E -1 ↾ A Part A ↔ Disj R ∩ E -1 ↾ A ∧ dom ⁡ R ∩ E -1 ↾ A / R ∩ E -1 ↾ A = A
3 dferALTV2 ⊢ ≀ R ∩ E -1 ↾ A ErALTV A ↔ EqvRel ≀ R ∩ E -1 ↾ A ∧ dom ⁡ ≀ R ∩ E -1 ↾ A / ≀ R ∩ E -1 ↾ A = A
4 1 2 3 3bitr4i ⊢ R ∩ E -1 ↾ A Part A ↔ ≀ R ∩ E -1 ↾ A ErALTV A