Theorem pet 38837

Description: Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 38826 (as opposed to petincnvepres 38835). 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 38437.

This theorem (together with pets 38838 and pet2 38836) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 38825, mpet2 38826 and mpet3 38822 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 38826), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 38826 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 38836	. 2 ⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
2		dfpart2 38755	. 2 ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
3		dferALTV2 38654	. 2 ⊢ ( ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴 ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))
4	1, 2, 3	3bitr4i 303	1 ⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   E cep 5530  ^◡ccnv 5630  dom cdm 5631   ↾ cres 5633   / cqs 8647   ⋉ cxrn 38162   ≀ ccoss 38163   EqvRel weqvrel 38180   ErALTV werALTV 38189   Disj wdisjALTV 38197   Part wpart 38202

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-eprel 5531  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fo 6505  df-fv 6507  df-1st 7947  df-2nd 7948  df-ec 8650  df-qs 8654  df-xrn 38347  df-coss 38396  df-refrel 38497  df-cnvrefrel 38512  df-symrel 38529  df-trrel 38559  df-eqvrel 38570  df-dmqs 38624  df-erALTV 38650  df-funALTV 38668  df-disjALTV 38691  df-eldisj 38693  df-part 38752

This theorem is referenced by:  pets  38838