Theorem iseriALT

Description: Alternate proof of iseri , avoiding the usage of mptru and T. as antecedent by using ax-mp and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	iseri.1	$$⊢\mathrm{Rel}R$$
	iseri.2	$$⊢xRy\to yRx$$
	iseri.3	$$⊢\left(xRy\wedge yRz\right)\to xRz$$
	iseri.4	$$⊢x\in A\leftrightarrow xRx$$
Assertion	iseriALT	$$⊢R\mathrm{Er}A$$

Proof

Step	Hyp	Ref	Expression
1		iseri.1	$$⊢\mathrm{Rel}R$$
2		iseri.2	$$⊢xRy\to yRx$$
3		iseri.3	$$⊢\left(xRy\wedge yRz\right)\to xRz$$
4		iseri.4	$$⊢x\in A\leftrightarrow xRx$$
5		id	$$⊢\mathrm{Rel}R\to \mathrm{Rel}R$$
6	2	adantl	$$⊢\left(\mathrm{Rel}R\wedge xRy\right)\to yRx$$
7	3	adantl	$$⊢\left(\mathrm{Rel}R\wedge \left(xRy\wedge yRz\right)\right)\to xRz$$
8	4	a1i	$$⊢\mathrm{Rel}R\to \left(x\in A\leftrightarrow xRx\right)$$
9	5 6 7 8	iserd	$$⊢\mathrm{Rel}R\to R\mathrm{Er}A$$
10	1 9	ax-mp	$$⊢R\mathrm{Er}A$$