seqex

Description: Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

		Ref	Expression
	Assertion	seqex	$⊢ seq M (\underset{˙}{+}, F) \in V$

Step	Hyp	Ref	Expression
1		df-seq	$⊢ seq M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
2		rdgfun	$⊢ Fun rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩)$
3		omex	$⊢ ω \in V$
4		funimaexg	$⊢ (Fun rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) \land ω \in V) \to rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω] \in V$
5	2 3 4	mp2an	$⊢ rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω] \in V$
6	1 5	eqeltri	$⊢ seq M (\underset{˙}{+}, F) \in V$

Metamath Proof Explorer