Metamath Proof Explorer


Theorem dfmembpart2

Description: Alternate definition of the conventional membership case of partition. Partition A of X , Halmos p. 28: "A partition of X is a disjoint collection A of non-empty subsets of X whose union is X ", or Definition 35, Suppes p. 83., cf. https://oeis.org/A000110 . (Contributed by Peter Mazsa, 14-Aug-2021)

Ref Expression
Assertion dfmembpart2
|- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) )

Proof

Step Hyp Ref Expression
1 df-membpart
 |-  ( MembPart A <-> ( `' _E |` A ) Part A )
2 df-part
 |-  ( ( `' _E |` A ) Part A <-> ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) )
3 df-eldisj
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
4 3 bicomi
 |-  ( Disj ( `' _E |` A ) <-> ElDisj A )
5 cnvepresdmqs
 |-  ( ( `' _E |` A ) DomainQs A <-> -. (/) e. A )
6 4 5 anbi12i
 |-  ( ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) <-> ( ElDisj A /\ -. (/) e. A ) )
7 1 2 6 3bitri
 |-  ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) )