noseqrdglem

Description: A helper lemma for the value of a recursive defintion generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	$⊢ φ \to C \in No$
	om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
	om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
	noseqrdg.1	$⊢ φ \to A \in V$
	noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
Assertion	noseqrdglem	$⊢ (φ \land B \in Z) \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
4		noseqrdg.1	$⊢ φ \to A \in V$
5		noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
6	1 2 3	om2noseqf1o	$⊢ φ \to G : ω \underset{1-1 onto}{⟶} Z$
7		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land B \in Z) \to G^{-1} (B) \in ω$
8	6 7	sylan	$⊢ (φ \land B \in Z) \to G^{-1} (B) \in ω$
9	1 2 3 4 5	om2noseqrdg	$⊢ (φ \land G^{-1} (B) \in ω) \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
10	8 9	syldan	$⊢ (φ \land B \in Z) \to R (G^{-1} (B)) = ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩$
11		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land B \in Z) \to G (G^{-1} (B)) = B$
12	6 11	sylan	$⊢ (φ \land B \in Z) \to G (G^{-1} (B)) = B$
13	12	opeq1d	$⊢ (φ \land B \in Z) \to ⟨G (G^{-1} (B)), 2^{nd} (R (G^{-1} (B)))⟩ = ⟨B, 2^{nd} (R (G^{-1} (B)))⟩$
14	10 13	eqtrd	$⊢ (φ \land B \in Z) \to R (G^{-1} (B)) = ⟨B, 2^{nd} (R (G^{-1} (B)))⟩$
15		frfnom	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω$
16	5	fneq1d	$⊢ φ \to (R Fn ω \leftrightarrow ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω)$
17	15 16	mpbiri	$⊢ φ \to R Fn ω$
18	17	adantr	$⊢ (φ \land B \in Z) \to R Fn ω$
19	18 8	fnfvelrnd	$⊢ (φ \land B \in Z) \to R (G^{-1} (B)) \in ran R$
20	14 19	eqeltrrd	$⊢ (φ \land B \in Z) \to ⟨B, 2^{nd} (R (G^{-1} (B)))⟩ \in ran R$

Metamath Proof Explorer

Theorem noseqrdglem

Proof