mpets

Description: Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet , the Partition-Equivalence Theorem, with general R . (Contributed by Peter Mazsa, 31-Dec-2024)

		Ref	Expression
	Assertion	mpets	⊢ MembParts = CoMembErs

Proof

Step	Hyp	Ref	Expression
1		mpets2	⊢ ( 𝑎 ∈ V → ( ( ^◡ E ↾ 𝑎 ) Parts 𝑎 ↔ ≀ ( ^◡ E ↾ 𝑎 ) Ers 𝑎 ) )
2	1	elv	⊢ ( ( ^◡ E ↾ 𝑎 ) Parts 𝑎 ↔ ≀ ( ^◡ E ↾ 𝑎 ) Ers 𝑎 )
3	2	abbii	⊢ { 𝑎 ∣ ( ^◡ E ↾ 𝑎 ) Parts 𝑎 } = { 𝑎 ∣ ≀ ( ^◡ E ↾ 𝑎 ) Ers 𝑎 }
4		df-membparts	⊢ MembParts = { 𝑎 ∣ ( ^◡ E ↾ 𝑎 ) Parts 𝑎 }
5		df-comembers	⊢ CoMembErs = { 𝑎 ∣ ≀ ( ^◡ E ↾ 𝑎 ) Ers 𝑎 }
6	3 4 5	3eqtr4i	⊢ MembParts = CoMembErs

Metamath Proof Explorer

Theorem mpets

Proof