Metamath Proof Explorer

Theorem om2noseq0

Description: The mapping G is a one-to-one mapping from _om onto a countable sequence of surreals that will be used to show the properties of seq_s . This theorem shows the value of G at ordinal zero. Compare the series of theorems starting at om2uz0i . (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) ↾}_{ω}$
Assertion	om2noseq0	$⊢ φ \to G (\emptyset) = C$

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	2	fveq1d	$⊢ φ \to G (\emptyset) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (\emptyset)$
4		fr0g	$⊢ C \in No \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (\emptyset) = C$
5	1 4	syl	$⊢ φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (\emptyset) = C$
6	3 5	eqtrd	$⊢ φ \to G (\emptyset) = C$