This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin1a2lem1

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

		Ref	Expression
	Hypothesis	fin1a2lem.a	$⊢ S = (x \in On ⟼ suc x)$
	Assertion	fin1a2lem1	$⊢ A \in On \to S (A) = suc A$

Step	Hyp	Ref	Expression
1		fin1a2lem.a	$⊢ S = (x \in On ⟼ suc x)$
2		onsuc	$⊢ A \in On \to suc A \in On$
3		suceq	$⊢ a = A \to suc a = suc A$
4		suceq	$⊢ x = a \to suc x = suc a$
5	4	cbvmptv	$⊢ (x \in On ⟼ suc x) = (a \in On ⟼ suc a)$
6	1 5	eqtri	$⊢ S = (a \in On ⟼ suc a)$
7	3 6	fvmptg	$⊢ (A \in On \land suc A \in On) \to S (A) = suc A$
8	2 7	mpdan	$⊢ A \in On \to S (A) = suc A$