Description: Define the member partition predicate, or the disjoint restricted element relation on its domain quotient predicate. (Read: A is a member partition.) A alternative definition is dfmembpart2 .
Member partition is the conventional meaning of partition (see the notes of df-parts and dfmembpart2 ), we generalize the concept in df-parts and df-part .
Member partition and comember equivalence are the same by mpet . (Contributed by Peter Mazsa, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-membpart | ⊢ ( MembPart 𝐴 ↔ ( ◡ E ↾ 𝐴 ) Part 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | 0 | wmembpart | ⊢ MembPart 𝐴 |
| 2 | cep | ⊢ E | |
| 3 | 2 | ccnv | ⊢ ◡ E |
| 4 | 3 0 | cres | ⊢ ( ◡ E ↾ 𝐴 ) |
| 5 | 0 4 | wpart | ⊢ ( ◡ E ↾ 𝐴 ) Part 𝐴 |
| 6 | 1 5 | wb | ⊢ ( MembPart 𝐴 ↔ ( ◡ E ↾ 𝐴 ) Part 𝐴 ) |