Theorem pet 40089

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

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   E cep 5554  ^◡ccnv 5654  dom cdm 5655   ↾ cres 5657   / cqs 8744   ⋉ cxrn 39298   ≀ ccoss 39307   EqvRel weqvrel 39324   ErALTV werALTV 39333   Disj wdisjALTV 39343   Part wpart 39348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-eprel 5555  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fo 6564  df-fv 6566  df-1st 8025  df-2nd 8026  df-ec 8747  df-qs 8751  df-xrn 39504  df-coss 39625  df-refrel 39716  df-cnvrefrel 39731  df-symrel 39748  df-trrel 39782  df-eqvrel 39793  df-dmqs 39847  df-erALTV 39873  df-funALTV 39891  df-disjALTV 39914  df-eldisj 39916  df-part 39993

This theorem is used by:  pets  40090