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	|- Rel R
	iseri.2	|- ( x R y -> y R x )
	iseri.3	|- ( ( x R y /\ y R z ) -> x R z )
	iseri.4	|- ( x e. A <-> x R x )
Assertion	iseriALT	|- R Er A

Proof

Step	Hyp	Ref	Expression
1		iseri.1	|- Rel R
2		iseri.2	|- ( x R y -> y R x )
3		iseri.3	|- ( ( x R y /\ y R z ) -> x R z )
4		iseri.4	|- ( x e. A <-> x R x )
5		id	|- ( Rel R -> Rel R )
6	2	adantl	|- ( ( Rel R /\ x R y ) -> y R x )
7	3	adantl	|- ( ( Rel R /\ ( x R y /\ y R z ) ) -> x R z )
8	4	a1i	|- ( Rel R -> ( x e. A <-> x R x ) )
9	5 6 7 8	iserd	|- ( Rel R -> R Er A )
10	1 9	ax-mp	|- R Er A