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 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )

Proof

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