Metamath Proof Explorer

Theorem seqex

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

Ref Expression
Assertion seqex ⊢ seq M + ˙ F ∈ V

Proof

Step Hyp Ref Expression
1 df-seq ⊢ seq M + ˙ F = rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 y + ˙ F ⁡ x + 1 M F ⁡ M ω
2 rdgfun ⊢ Fun ⁡ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 y + ˙ F ⁡ x + 1 M F ⁡ M
3 omex ⊢ ω ∈ V
4 funimaexg ⊢ Fun ⁡ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 y + ˙ F ⁡ x + 1 M F ⁡ M ∧ ω ∈ V → rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 y + ˙ F ⁡ x + 1 M F ⁡ M ω ∈ V
5 2 3 4 mp2an ⊢ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 y + ˙ F ⁡ x + 1 M F ⁡ M ω ∈ V
6 1 5 eqeltri ⊢ seq M + ˙ F ∈ V