noseqp1

Description: One plus an element of Z is an element of Z . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
	noseq.2	$⊢ φ \to A \in No$
	noseqp1.3	$⊢ φ \to B \in Z$
Assertion	noseqp1	$⊢ φ \to B +_{s} 1_{s} \in Z$

Proof

Step	Hyp	Ref	Expression
1		noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
2		noseq.2	$⊢ φ \to A \in No$
3		noseqp1.3	$⊢ φ \to B \in Z$
4	3 1	eleqtrd	$⊢ φ \to B \in rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
5		df-ima	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω] = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
6	4 5	eleqtrdi	$⊢ φ \to B \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
7		frfnom	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) Fn ω$
8		fvelrnb	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) Fn ω \to (B \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B)$
9	7 8	ax-mp	$⊢ B \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B$
10	6 9	sylib	$⊢ φ \to \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B$
11		ovex	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s} \in V$
12		eqid	$⊢ {rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω} = {rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}$
13		oveq1	$⊢ z = x \to z +_{s} 1_{s} = x +_{s} 1_{s}$
14		oveq1	$⊢ z = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) \to z +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s}$
15	12 13 14	frsucmpt2	$⊢ (y \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s} \in V) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s}$
16	11 15	mpan2	$⊢ y \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s}$
17	16	adantl	$⊢ (φ \land y \in ω) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s}$
18		peano2	$⊢ y \in ω \to suc y \in ω$
19		fnfvelrn	$⊢ (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) Fn ω \land suc y \in ω) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
20	7 18 19	sylancr	$⊢ y \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
21	20	adantl	$⊢ (φ \land y \in ω) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
22	1 5	eqtrdi	$⊢ φ \to Z = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
23	22	adantr	$⊢ (φ \land y \in ω) \to Z = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
24	21 23	eleqtrrd	$⊢ (φ \land y \in ω) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc y) \in Z$
25	17 24	eqeltrrd	$⊢ (φ \land y \in ω) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s} \in Z$
26		oveq1	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s} = B +_{s} 1_{s}$
27	26	eleq1d	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) +_{s} 1_{s} \in Z \leftrightarrow B +_{s} 1_{s} \in Z)$
28	25 27	syl5ibcom	$⊢ (φ \land y \in ω) \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B \to B +_{s} 1_{s} \in Z)$
29	28	impr	$⊢ (φ \land (y \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (y) = B)) \to B +_{s} 1_{s} \in Z$
30	10 29	rexlimddv	$⊢ φ \to B +_{s} 1_{s} \in Z$

Metamath Proof Explorer

Theorem noseqp1

Proof