Theorem mpet3

Description: Member Partition-Equivalence Theorem. Together with mpet mpet2 , mostly in its conventional cpet and cpet2 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 4-May-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	mpet3	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjn0elb	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( Disj ( ◡ E ↾ 𝐴 ) ∧ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
2		eqvrelqseqdisj3	⊢ ( ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) → Disj ( ◡ E ↾ 𝐴 ) )
3	2	petlem	⊢ ( ( Disj ( ◡ E ↾ 𝐴 ) ∧ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) ↔ ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
4		eqvreldmqs	⊢ ( ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
5	1 3 4	3bitri	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )