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 𝑅
	iseri.2	⊢ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 )
	iseri.3	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
	iseri.4	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 )
Assertion	iseriALT	⊢ 𝑅 Er 𝐴

Proof

Step	Hyp	Ref	Expression
1		iseri.1	⊢ Rel 𝑅
2		iseri.2	⊢ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 )
3		iseri.3	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
4		iseri.4	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 )
5		id	⊢ ( Rel 𝑅 → Rel 𝑅 )
6	2	adantl	⊢ ( ( Rel 𝑅 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 𝑅 𝑥 )
7	3	adantl	⊢ ( ( Rel 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 )
8	4	a1i	⊢ ( Rel 𝑅 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 ) )
9	5 6 7 8	iserd	⊢ ( Rel 𝑅 → 𝑅 Er 𝐴 )
10	1 9	ax-mp	⊢ 𝑅 Er 𝐴

Metamath Proof Explorer

Theorem iseriALT

Proof