Metamath Proof Explorer

Theorem oasuc

Description: Addition with successor. Definition 8.1 of TakeutiZaring p. 56. Definition 2.3 of Schloeder p. 4. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oasuc	$⊢ (A \in On \land B \in On) \to A +_{𝑜} suc B = suc (A +_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		rdgsuc	$⊢ B \in On \to rec ((x \in V ⟼ suc x), A) (suc B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
2	1	adantl	$⊢ (A \in On \land B \in On) \to rec ((x \in V ⟼ suc x), A) (suc B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
3		onsuc	$⊢ B \in On \to suc B \in On$
4		oav	$⊢ (A \in On \land suc B \in On) \to A +_{𝑜} suc B = rec ((x \in V ⟼ suc x), A) (suc B)$
5	3 4	sylan2	$⊢ (A \in On \land B \in On) \to A +_{𝑜} suc B = rec ((x \in V ⟼ suc x), A) (suc B)$
6		ovex	$⊢ A +_{𝑜} B \in V$
7		suceq	$⊢ x = A +_{𝑜} B \to suc x = suc (A +_{𝑜} B)$
8		eqid	$⊢ (x \in V ⟼ suc x) = (x \in V ⟼ suc x)$
9	6	sucex	$⊢ suc (A +_{𝑜} B) \in V$
10	7 8 9	fvmpt	$⊢ A +_{𝑜} B \in V \to (x \in V ⟼ suc x) (A +_{𝑜} B) = suc (A +_{𝑜} B)$
11	6 10	ax-mp	$⊢ (x \in V ⟼ suc x) (A +_{𝑜} B) = suc (A +_{𝑜} B)$
12		oav	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B = rec ((x \in V ⟼ suc x), A) (B)$
13	12	fveq2d	$⊢ (A \in On \land B \in On) \to (x \in V ⟼ suc x) (A +_{𝑜} B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
14	11 13	eqtr3id	$⊢ (A \in On \land B \in On) \to suc (A +_{𝑜} B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
15	2 5 14	3eqtr4d	$⊢ (A \in On \land B \in On) \to A +_{𝑜} suc B = suc (A +_{𝑜} B)$