This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfseq

Description: Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nfseq.1 ⊢ Ⅎ _ x M
nfseq.2 ⊢ Ⅎ _ x + ˙
nfseq.3 ⊢ Ⅎ _ x F
Assertion nfseq ⊢ Ⅎ _ x seq M + ˙ F

Proof

Step Hyp Ref Expression
1 nfseq.1 ⊢ Ⅎ _ x M
2 nfseq.2 ⊢ Ⅎ _ x + ˙
3 nfseq.3 ⊢ Ⅎ _ x F
4 df-seq ⊢ seq M + ˙ F = rec ⁡ z ∈ V , w ∈ V ⟼ z + 1 w + ˙ F ⁡ z + 1 M F ⁡ M ω
5 nfcv ⊢ Ⅎ _ x V
6 nfcv ⊢ Ⅎ _ x z + 1
7 nfcv ⊢ Ⅎ _ x w
8 3 6 nffv ⊢ Ⅎ _ x F ⁡ z + 1
9 7 2 8 nfov ⊢ Ⅎ _ x w + ˙ F ⁡ z + 1
10 6 9 nfop ⊢ Ⅎ _ x z + 1 w + ˙ F ⁡ z + 1
11 5 5 10 nfmpo ⊢ Ⅎ _ x z ∈ V , w ∈ V ⟼ z + 1 w + ˙ F ⁡ z + 1
12 3 1 nffv ⊢ Ⅎ _ x F ⁡ M
13 1 12 nfop ⊢ Ⅎ _ x M F ⁡ M
14 11 13 nfrdg ⊢ Ⅎ _ x rec ⁡ z ∈ V , w ∈ V ⟼ z + 1 w + ˙ F ⁡ z + 1 M F ⁡ M
15 nfcv ⊢ Ⅎ _ x ω
16 14 15 nfima ⊢ Ⅎ _ x rec ⁡ z ∈ V , w ∈ V ⟼ z + 1 w + ˙ F ⁡ z + 1 M F ⁡ M ω
17 4 16 nfcxfr ⊢ Ⅎ _ x seq M + ˙ F