| Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > pets | Structured version Visualization version GIF version | ||
| Description: Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 39283 and pet2 39282) is the main result of my investigation into set theory, cf. the comment of pet 39283. (Contributed by Peter Mazsa, 23-Sep-2021.) |
| Ref | Expression |
|---|---|
| pets | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pet 39283 | . 2 ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴) | |
| 2 | xrncnvepresex 38749 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) | |
| 3 | brpartspart 39194 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ (𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴)) | |
| 4 | 2, 3 | syldan 592 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ (𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴)) |
| 5 | 1cossxrncnvepresex 38830 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) | |
| 6 | brerser 39080 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∈ V) → ( ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴)) | |
| 7 | 5, 6 | syldan 592 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ( ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴)) |
| 8 | 4, 7 | bibi12d 345 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴) ↔ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴))) |
| 9 | 1, 8 | mpbiri 258 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2114 Vcvv 3430 class class class wbr 5086 E cep 5527 ◡ccnv 5627 ↾ cres 5630 ⋉ cxrn 38492 ≀ ccoss 38501 Ers cers 38526 ErALTV werALTV 38527 Parts cparts 38541 Part wpart 38542 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5306 ax-pr 5374 ax-un 7686 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5523 df-eprel 5528 df-xp 5634 df-rel 5635 df-cnv 5636 df-co 5637 df-dm 5638 df-rn 5639 df-res 5640 df-ima 5641 df-iota 6452 df-fun 6498 df-fn 6499 df-f 6500 df-fo 6502 df-fv 6504 df-1st 7939 df-2nd 7940 df-ec 8642 df-qs 8646 df-xrn 38698 df-rels 38758 df-coss 38819 df-ssr 38896 df-refs 38908 df-refrels 38909 df-refrel 38910 df-cnvrefs 38923 df-cnvrefrels 38924 df-cnvrefrel 38925 df-syms 38940 df-symrels 38941 df-symrel 38942 df-trs 38974 df-trrels 38975 df-trrel 38976 df-eqvrels 38986 df-eqvrel 38987 df-dmqss 39040 df-dmqs 39041 df-ers 39066 df-erALTV 39067 df-funALTV 39085 df-disjss 39106 df-disjs 39107 df-disjALTV 39108 df-eldisj 39110 df-parts 39186 df-part 39187 |
| This theorem is referenced by: typesafepets 39293 |
| Copyright terms: Public domain | W3C validator |