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 ∧ ¬ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 df-membpart ⊢ MembPart A ↔ E -1 ↾ A Part A
2 df-part ⊢ E -1 ↾ A Part A ↔ Disj E -1 ↾ A ∧ E -1 ↾ A DomainQs A
3 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
4 3 bicomi ⊢ Disj E -1 ↾ A ↔ ElDisj A
5 cnvepresdmqs ⊢ E -1 ↾ A DomainQs A ↔ ¬ ∅ ∈ A
6 4 5 anbi12i ⊢ Disj E -1 ↾ A ∧ E -1 ↾ A DomainQs A ↔ ElDisj A ∧ ¬ ∅ ∈ A
7 1 2 6 3bitri ⊢ MembPart A ↔ ElDisj A ∧ ¬ ∅ ∈ A