| 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 38818 mpet2 38819, mostly in its conventional cpet 38817 and cpet2 38816 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38829 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 38724 | . 2 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)) | |
| 2 | eqvrelqseqdisj3 38810 | . . 3 ⊢ (( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴) → Disj (◡ E ↾ 𝐴)) | |
| 3 | 2 | petlem 38791 | . 2 ⊢ (( Disj (◡ E ↾ 𝐴) ∧ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ≀ (◡ E ↾ 𝐴) ∧ (dom ≀ (◡ E ↾ 𝐴) / ≀ (◡ E ↾ 𝐴)) = 𝐴)) |
| 4 | eqvreldmqs 38654 | . 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 1540 ∈ wcel 2108 ∅c0 4332 ∪ cuni 4905 E cep 5581 ◡ccnv 5682 dom cdm 5683 ↾ cres 5685 / cqs 8740 ≀ ccoss 38160 ∼ ccoels 38161 EqvRel weqvrel 38177 CoElEqvRel wcoeleqvrel 38179 Disj wdisjALTV 38194 ElDisj weldisj 38196 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5294 ax-nul 5304 ax-pr 5430 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3379 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-br 5142 df-opab 5204 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 8743 df-qs 8747 df-coss 38390 df-coels 38391 df-refrel 38491 df-cnvrefrel 38506 df-symrel 38523 df-trrel 38553 df-eqvrel 38564 df-coeleqvrel 38566 df-funALTV 38661 df-disjALTV 38684 df-eldisj 38686 |
| This theorem is referenced by: mpet 38818 |
| Copyright terms: Public domain | W3C validator |