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