onasuc

Description: Addition with successor. Theorem 4I(A2) of Enderton p. 79. (Note that this version of oasuc does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		frsuc	$⊢ B \in ω \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 ω) \to ({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (suc B) = (x \in V ⟼ suc x) (({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (B))$
3		peano2	$⊢ B \in ω \to suc B \in ω$
4	3	adantl	$⊢ (A \in On \land B \in ω) \to suc B \in ω$
5	4	fvresd	$⊢ (A \in On \land B \in ω) \to ({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (suc B) = rec ((x \in V ⟼ suc x), A) (suc B)$
6		fvres	$⊢ B \in ω \to ({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (B) = rec ((x \in V ⟼ suc x), A) (B)$
7	6	adantl	$⊢ (A \in On \land B \in ω) \to ({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (B) = rec ((x \in V ⟼ suc x), A) (B)$
8	7	fveq2d	$⊢ (A \in On \land B \in ω) \to (x \in V ⟼ suc x) (({rec ((x \in V ⟼ suc x), A) ↾}_{ω}) (B)) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
9	2 5 8	3eqtr3d	$⊢ (A \in On \land B \in ω) \to rec ((x \in V ⟼ suc x), A) (suc B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
10		nnon	$⊢ B \in ω \to B \in On$
11		onsuc	$⊢ B \in On \to suc B \in On$
12	10 11	syl	$⊢ B \in ω \to suc B \in On$
13		oav	$⊢ (A \in On \land suc B \in On) \to A +_{𝑜} suc B = rec ((x \in V ⟼ suc x), A) (suc B)$
14	12 13	sylan2	$⊢ (A \in On \land B \in ω) \to A +_{𝑜} suc B = rec ((x \in V ⟼ suc x), A) (suc B)$
15		ovex	$⊢ A +_{𝑜} B \in V$
16		suceq	$⊢ x = A +_{𝑜} B \to suc x = suc (A +_{𝑜} B)$
17		eqid	$⊢ (x \in V ⟼ suc x) = (x \in V ⟼ suc x)$
18	15	sucex	$⊢ suc (A +_{𝑜} B) \in V$
19	16 17 18	fvmpt	$⊢ A +_{𝑜} B \in V \to (x \in V ⟼ suc x) (A +_{𝑜} B) = suc (A +_{𝑜} B)$
20	15 19	ax-mp	$⊢ (x \in V ⟼ suc x) (A +_{𝑜} B) = suc (A +_{𝑜} B)$
21		oav	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B = rec ((x \in V ⟼ suc x), A) (B)$
22	10 21	sylan2	$⊢ (A \in On \land B \in ω) \to A +_{𝑜} B = rec ((x \in V ⟼ suc x), A) (B)$
23	22	fveq2d	$⊢ (A \in On \land B \in ω) \to (x \in V ⟼ suc x) (A +_{𝑜} B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
24	20 23	eqtr3id	$⊢ (A \in On \land B \in ω) \to suc (A +_{𝑜} B) = (x \in V ⟼ suc x) (rec ((x \in V ⟼ suc x), A) (B))$
25	9 14 24	3eqtr4d	$⊢ (A \in On \land B \in ω) \to A +_{𝑜} suc B = suc (A +_{𝑜} B)$

Metamath Proof Explorer

Theorem onasuc

Proof