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

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 ) )