Theorem mpet3 38775

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

Assertion

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

Proof of Theorem mpet3

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∅c0 4306  ∪ cuni 4880   E cep 5549  ^◡ccnv 5650  dom cdm 5651   ↾ cres 5653   / cqs 8712   ≀ ccoss 38120   ∼ ccoels 38121   EqvRel weqvrel 38137   CoElEqvRel wcoeleqvrel 38139   Disj wdisjALTV 38154   ElDisj weldisj 38156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3357  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-id 5545  df-eprel 5550  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ec 8715  df-qs 8719  df-coss 38350  df-coels 38351  df-refrel 38451  df-cnvrefrel 38466  df-symrel 38483  df-trrel 38513  df-eqvrel 38524  df-coeleqvrel 38526  df-funALTV 38621  df-disjALTV 38644  df-eldisj 38646

This theorem is referenced by:  mpet  38778