Theorem mainpart

Description: Partition with general R also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021) (Revised by Peter Mazsa, 22-Dec-2024)

	Ref	Expression
Assertion	mainpart	Could not format assertion : No typesetting found for |- ( R Part A -> MembPart A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		partimcomember	Could not format ( R Part A -> CoMembEr A ) : No typesetting found for |- ( R Part A -> CoMembEr A ) with typecode |-
2		mpet	Could not format ( MembPart A <-> CoMembEr A ) : No typesetting found for |- ( MembPart A <-> CoMembEr A ) with typecode |-
3	1 2	sylibr	Could not format ( R Part A -> MembPart A ) : No typesetting found for |- ( R Part A -> MembPart A ) with typecode |-