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	$$⊢\left(A\in \mathrm{MembParts}\wedge R\in V\right)\to \left(R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Parts}A\leftrightarrow \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Ers}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pets	$$⊢\left(A\in \mathrm{MembParts}\wedge R\in V\right)\to \left(R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Parts}A\leftrightarrow \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Ers}A\right)$$