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	Could not format assertion : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-membpart	Could not format ( MembPart A <-> ( `' _E |` A ) Part A ) : No typesetting found for |- ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode |-
2		df-part	Could not format ( ( `' _E |` A ) Part A <-> ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) ) : No typesetting found for |- ( ( `' _E |` A ) Part A <-> ( Disj ( `' _E |` A ) /\ ( `' _E |` A ) DomainQs A ) ) with typecode |-
3		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
4	3	bicomi	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow ElDisjA$$
5		cnvepresdmqs	$$⊢\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)DomainQsA\leftrightarrow \neg \varnothing \in A$$
6	4 5	anbi12i	$$⊢\left(Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\wedge \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)DomainQsA\right)\leftrightarrow \left(ElDisjA\wedge \neg \varnothing \in A\right)$$
7	1 2 6	3bitri	Could not format ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) : No typesetting found for |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) with typecode |-