![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > mpet3 | Structured version Visualization version GIF version |
Description: Member Partition-Equivalence Theorem. Together with mpet 38782 mpet2 38783, mostly in its conventional cpet 38781 and cpet2 38780 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38793 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
Ref | Expression |
---|---|
mpet3 | ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldisjn0elb 38688 | . 2 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)) | |
2 | eqvrelqseqdisj3 38774 | . . 3 ⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) → Disj (◡ E ↾ 𝐴)) | |
3 | 2 | petlem 38755 | . 2 ⊢ (( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴)) |
4 | eqvreldmqs 38618 | . 2 ⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | |
5 | 1, 3, 4 | 3bitri 297 | 1 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1535 ∈ wcel 2104 ∅c0 4339 ∪ cuni 4914 E cep 5581 ◡ccnv 5682 dom cdm 5683 ↾ cres 5685 / cqs 8737 ≀ ccoss 38122 ∼ ccoels 38123 EqvRel weqvrel 38139 CoElEqvRel wcoeleqvrel 38141 Disj wdisjALTV 38156 ElDisj weldisj 38158 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5430 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-ral 3058 df-rex 3067 df-rmo 3376 df-rab 3433 df-v 3479 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4915 df-br 5150 df-opab 5212 df-id 5576 df-eprel 5582 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-ec 8740 df-qs 8744 df-coss 38354 df-coels 38355 df-refrel 38455 df-cnvrefrel 38470 df-symrel 38487 df-trrel 38517 df-eqvrel 38528 df-coeleqvrel 38530 df-funALTV 38625 df-disjALTV 38648 df-eldisj 38650 |
This theorem is referenced by: mpet 38782 |
Copyright terms: Public domain | W3C validator |