Description: Class A is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pet0 | |- ( (/) Part A <-> ,~ (/) ErALTV A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pet02 | |- ( ( Disj (/) /\ ( dom (/) /. (/) ) = A ) <-> ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) |
|
| 2 | dfpart2 | |- ( (/) Part A <-> ( Disj (/) /\ ( dom (/) /. (/) ) = A ) ) |
|
| 3 | dferALTV2 | |- ( ,~ (/) ErALTV A <-> ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) |
|
| 4 | 1 2 3 | 3bitr4i | |- ( (/) Part A <-> ,~ (/) ErALTV A ) |