This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cpet2

Description: The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet . Together with cpet , mpet mpet2 , this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 30-Dec-2024)

Ref Expression
Assertion cpet2 ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

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 eqvreldmqs2 ⊢ ( ( EqvRel ≀ ( ◡ E ↾ 𝐴 ) ∧ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
5 1 3 4 3bitri ⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ↔ ( EqvRel ∼ 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )