Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pets Structured version   Visualization version   GIF version

Theorem pets 39246
Description: Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 39245 and pet2 39244) is the main result of my investigation into set theory, cf. the comment of pet 39245. (Contributed by Peter Mazsa, 23-Sep-2021.)
Assertion
Ref Expression
pets ((𝐴𝑉𝑅𝑊) → ((𝑅 ⋉ ( E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) Ers 𝐴))

Proof of Theorem pets
StepHypRef Expression
1 pet 39245 . 2 ((𝑅 ⋉ ( E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ErALTV 𝐴)
2 xrncnvepresex 38711 . . . 4 ((𝐴𝑉𝑅𝑊) → (𝑅 ⋉ ( E ↾ 𝐴)) ∈ V)
3 brpartspart 39156 . . . 4 ((𝐴𝑉 ∧ (𝑅 ⋉ ( E ↾ 𝐴)) ∈ V) → ((𝑅 ⋉ ( E ↾ 𝐴)) Parts 𝐴 ↔ (𝑅 ⋉ ( E ↾ 𝐴)) Part 𝐴))
42, 3syldan 592 . . 3 ((𝐴𝑉𝑅𝑊) → ((𝑅 ⋉ ( E ↾ 𝐴)) Parts 𝐴 ↔ (𝑅 ⋉ ( E ↾ 𝐴)) Part 𝐴))
5 1cossxrncnvepresex 38792 . . . 4 ((𝐴𝑉𝑅𝑊) → ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ∈ V)
6 brerser 39042 . . . 4 ((𝐴𝑉 ∧ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ∈ V) → ( ≀ (𝑅 ⋉ ( E ↾ 𝐴)) Ers 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ErALTV 𝐴))
75, 6syldan 592 . . 3 ((𝐴𝑉𝑅𝑊) → ( ≀ (𝑅 ⋉ ( E ↾ 𝐴)) Ers 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ErALTV 𝐴))
84, 7bibi12d 345 . 2 ((𝐴𝑉𝑅𝑊) → (((𝑅 ⋉ ( E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) Ers 𝐴) ↔ ((𝑅 ⋉ ( E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) ErALTV 𝐴)))
91, 8mpbiri 258 1 ((𝐴𝑉𝑅𝑊) → ((𝑅 ⋉ ( E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ ( E ↾ 𝐴)) Ers 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2114  Vcvv 3442   class class class wbr 5100   E cep 5533  ccnv 5633  cres 5636  cxrn 38454  ccoss 38463   Ers cers 38488   ErALTV werALTV 38489   Parts cparts 38503   Part wpart 38504
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 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692
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 3352  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-eprel 5534  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fo 6508  df-fv 6510  df-1st 7945  df-2nd 7946  df-ec 8649  df-qs 8653  df-xrn 38660  df-rels 38720  df-coss 38781  df-ssr 38858  df-refs 38870  df-refrels 38871  df-refrel 38872  df-cnvrefs 38885  df-cnvrefrels 38886  df-cnvrefrel 38887  df-syms 38902  df-symrels 38903  df-symrel 38904  df-trs 38936  df-trrels 38937  df-trrel 38938  df-eqvrels 38948  df-eqvrel 38949  df-dmqss 39002  df-dmqs 39003  df-ers 39028  df-erALTV 39029  df-funALTV 39047  df-disjss 39068  df-disjs 39069  df-disjALTV 39070  df-eldisj 39072  df-parts 39148  df-part 39149
This theorem is referenced by:  typesafepets  39255
  Copyright terms: Public domain W3C validator