Theorem pets

Description: Partition-Equivalence Theorem with general R , with binary relations. This theorem (together with pet and pet2 ) is the main result of my investigation into set theory, cf. the comment of pet . (Contributed by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	pets	Could not format assertion : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pet	Could not format ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) : No typesetting found for |- ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) with typecode |-
2		xrncnvepresex	$$⊢\left(A\in V\wedge R\in W\right)\to R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$
3		brpartspart	Could not format ( ( A e. V /\ ( R |X. ( `' _E |` A ) ) e. _V ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) ) : No typesetting found for |- ( ( A e. V /\ ( R |X. ( `' _E |` A ) ) e. _V ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) ) with typecode |-
4	2 3	syldan	Could not format ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ( R |X. ( `' _E |` A ) ) Part A ) ) with typecode |-
5		1cossxrncnvepresex	$$⊢\left(A\in V\wedge R\in W\right)\to \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}$$
6		brerser	$$⊢\left(A\in V\wedge \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\in \mathrm{V}\right)\to \left(\wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Ers}A\leftrightarrow \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)ErALTVA\right)$$
7	5 6	syldan	$$⊢\left(A\in V\wedge R\in W\right)\to \left(\wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\mathrm{Ers}A\leftrightarrow \wr R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)ErALTVA\right)$$
8	4 7	bibi12d	Could not format ( ( A e. V /\ R e. W ) -> ( ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) <-> ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) <-> ( ( R |X. ( `' _E |` A ) ) Part A <-> ,~ ( R |X. ( `' _E |` A ) ) ErALTV A ) ) ) with typecode |-
9	1 8	mpbiri	Could not format ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) ) : No typesetting found for |- ( ( A e. V /\ R e. W ) -> ( ( R |X. ( `' _E |` A ) ) Parts A <-> ,~ ( R |X. ( `' _E |` A ) ) Ers A ) ) with typecode |-