Theorem antisymrelres

Description: (Contributed by Peter Mazsa, 25-Jun-2024)

	Ref	Expression
Assertion	antisymrelres	Could not format assertion : No typesetting found for |- ( AntisymRel ( R |` A ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_A\right)$$
2		dfantisymrel5	Could not format ( AntisymRel ( R |` A ) <-> ( A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) /\ Rel ( R |` A ) ) ) : No typesetting found for |- ( AntisymRel ( R |` A ) <-> ( A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) /\ Rel ( R |` A ) ) ) with typecode |-
3	1 2	mpbiran2	Could not format ( AntisymRel ( R |` A ) <-> A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) ) : No typesetting found for |- ( AntisymRel ( R |` A ) <-> A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) ) with typecode |-
4		brres	$$⊢y\in \mathrm{V}\to \left(x\left({R\upharpoonright }_A\right)y\leftrightarrow \left(x\in A\wedge xRy\right)\right)$$
5	4	elv	$$⊢x\left({R\upharpoonright }_A\right)y\leftrightarrow \left(x\in A\wedge xRy\right)$$
6		brres	$$⊢x\in \mathrm{V}\to \left(y\left({R\upharpoonright }_A\right)x\leftrightarrow \left(y\in A\wedge yRx\right)\right)$$
7	6	elv	$$⊢y\left({R\upharpoonright }_A\right)x\leftrightarrow \left(y\in A\wedge yRx\right)$$
8	5 7	anbi12i	$$⊢\left(x\left({R\upharpoonright }_A\right)y\wedge y\left({R\upharpoonright }_A\right)x\right)\leftrightarrow \left(\left(x\in A\wedge xRy\right)\wedge \left(y\in A\wedge yRx\right)\right)$$
9		an4	$$⊢\left(\left(x\in A\wedge xRy\right)\wedge \left(y\in A\wedge yRx\right)\right)\leftrightarrow \left(\left(x\in A\wedge y\in A\right)\wedge \left(xRy\wedge yRx\right)\right)$$
10	8 9	bitri	$$⊢\left(x\left({R\upharpoonright }_A\right)y\wedge y\left({R\upharpoonright }_A\right)x\right)\leftrightarrow \left(\left(x\in A\wedge y\in A\right)\wedge \left(xRy\wedge yRx\right)\right)$$
11	10	imbi1i	$$⊢\left(\left(x\left({R\upharpoonright }_A\right)y\wedge y\left({R\upharpoonright }_A\right)x\right)\to x=y\right)\leftrightarrow \left(\left(\left(x\in A\wedge y\in A\right)\wedge \left(xRy\wedge yRx\right)\right)\to x=y\right)$$
12	11	2albii	$$⊢\forall x\forall y\left(\left(x\left({R\upharpoonright }_A\right)y\wedge y\left({R\upharpoonright }_A\right)x\right)\to x=y\right)\leftrightarrow \forall x\forall y\left(\left(\left(x\in A\wedge y\in A\right)\wedge \left(xRy\wedge yRx\right)\right)\to x=y\right)$$
13		r2alan	$$⊢\forall x\forall y\left(\left(\left(x\in A\wedge y\in A\right)\wedge \left(xRy\wedge yRx\right)\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(\left(xRy\wedge yRx\right)\to x=y\right)$$
14	3 12 13	3bitri	Could not format ( AntisymRel ( R |` A ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) ) : No typesetting found for |- ( AntisymRel ( R |` A ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) ) with typecode |-