Theorem pet 39582

Description: Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 39571 (as opposed to petincnvepres 39580). A class is a partition by a range Cartesian product with general 𝑅 and the restricted converse element class if and only if the cosets by the range Cartesian product are in an equivalence relation on it. Cf. br1cossxrncnvepres 39159.

This theorem (together with pets 39583 and pet2 39581) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 39570, mpet2 39571 and mpet3 39567 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 39571), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 39571 lacks: 𝑅, which is sufficient for my future application of set theory, for my purpose outside of set theory. (Contributed by Peter Mazsa, 23-Sep-2021.)

Assertion

Ref	Expression
pet	⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴)

Proof of Theorem pet

Step	Hyp	Ref	Expression
1		pet2 39581	. 2 ⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
2		dfpart2 39489	. 2 ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
3		dferALTV2 39370	. 2 ⊢ ( ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴 ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
4	1, 2, 3	3bitr4i 306	1 ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1568   E cep 5560  ^◡ccnv 5660  dom cdm 5661   ↾ cres 5663   / cqs 8692   ⋉ cxrn 38791   ≀ ccoss 38800   EqvRel weqvrel 38817   ErALTV werALTV 38826   Disj wdisjALTV 38836   Part wpart 38841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3367  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-eprel 5561  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fo 6542  df-fv 6544  df-1st 7985  df-2nd 7986  df-ec 8695  df-qs 8699  df-xrn 38997  df-coss 39118  df-refrel 39209  df-cnvrefrel 39224  df-symrel 39241  df-trrel 39275  df-eqvrel 39286  df-dmqs 39340  df-erALTV 39366  df-funALTV 39384  df-disjALTV 39407  df-eldisj 39409  df-part 39486

This theorem is referenced by:  pets  39583