Theorem typesafepets

Description: Type-safe pets scheme. On a membership block-carrier A e. MembParts , the lifted span ( R |X. (`' _E |`A ) ) yields a generalized partition of A iff its coset relation yields an equivalence relation on the same carrier A . This is the type-safe replacement for the earlier broad pets : it explicitly restricts to carriers where A is already known to be a block-family (by MembParts ). That removes the standard type-safety objection ("are you equating a quotient-carrier of blocks with raw witnesses?") by construction. It is the key bridge used to identify the partition-side and equivalence-side pet classes ( petseq ), in complete parallel with the membership bridge mpets . This theorem is intentionally not the definition of PetParts ; it is the bridge used by petseq after typedness is enforced by the "Pet*" definitions. (Contributed by Peter Mazsa, 19-Feb-2026)

	Ref	Expression
Assertion	typesafepets	|- ( ( A e. MembParts /\ R e. V ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) )

Proof

Step	Hyp	Ref	Expression
1		pets	|- ( ( A e. MembParts /\ R e. V ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) )