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

Metamath Proof Explorer

Theorem partsuc

Description: Property of the partition. (Contributed by Peter Mazsa, 20-Sep-2024)

Ref Expression
Assertion partsuc ⊢ R ↾ suc ⁡ A ∖ R ↾ A Part suc ⁡ A ∖ A ↔ R ↾ A Part A

Proof

Step Hyp Ref Expression
1 ressucdifsn ⊢ R ↾ suc ⁡ A ∖ R ↾ A = R ↾ A
2 sucdifsn ⊢ suc ⁡ A ∖ A = A
3 parteq12 ⊢ R ↾ suc ⁡ A ∖ R ↾ A = R ↾ A ∧ suc ⁡ A ∖ A = A → R ↾ suc ⁡ A ∖ R ↾ A Part suc ⁡ A ∖ A ↔ R ↾ A Part A
4 1 2 3 mp2an ⊢ R ↾ suc ⁡ A ∖ R ↾ A Part suc ⁡ A ∖ A ↔ R ↾ A Part A