Theorem pet2 38595

Description: Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 38596 and pets 38597) is the main result of my investigation into set theory, see the comment of pet 38596. (Contributed by Peter Mazsa, 24-May-2021.) (Revised by Peter Mazsa, 23-Sep-2021.)

Assertion

Ref	Expression
pet2	⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))

Proof of Theorem pet2

Step	Hyp	Ref	Expression
1		eqvrelqseqdisj5 38578	. 2 ⊢ (( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) → Disj (𝑅 ⋉ (◡ E ↾ 𝐴)))
2	1	petlem 38557	1 ⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1534   E cep 5589  ^◡ccnv 5685  dom cdm 5686   ↾ cres 5688   / cqs 8741   ⋉ cxrn 37922   ≀ ccoss 37923   EqvRel weqvrel 37940   Disj wdisjALTV 37957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437  ax-un 7751

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-rmo 3373  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-eprel 5590  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-fo 6564  df-fv 6566  df-1st 8011  df-2nd 8012  df-ec 8744  df-qs 8748  df-xrn 38116  df-coss 38156  df-refrel 38257  df-cnvrefrel 38272  df-symrel 38289  df-trrel 38319  df-eqvrel 38330  df-funALTV 38427  df-disjALTV 38450  df-eldisj 38452

This theorem is referenced by:  pet  38596