Metamath Proof Explorer


Theorem finxpreclem5

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis finxpreclem5.1 F = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
Assertion finxpreclem5 n ω 1 𝑜 n ¬ x V × U F n x = n x

Proof

Step Hyp Ref Expression
1 finxpreclem5.1 F = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
2 df-ov n F x = F n x
3 vex x V
4 0ex V
5 opex n 1 st x V
6 opex n x V
7 5 6 ifex if x V × U n 1 st x n x V
8 4 7 ifex if n = 1 𝑜 x U if x V × U n 1 st x n x V
9 1 ovmpt4g n ω x V if n = 1 𝑜 x U if x V × U n 1 st x n x V n F x = if n = 1 𝑜 x U if x V × U n 1 st x n x
10 3 8 9 mp3an23 n ω n F x = if n = 1 𝑜 x U if x V × U n 1 st x n x
11 10 ad2antrr n ω 1 𝑜 n ¬ x V × U n F x = if n = 1 𝑜 x U if x V × U n 1 st x n x
12 1on 1 𝑜 On
13 12 onirri ¬ 1 𝑜 1 𝑜
14 eleq2 n = 1 𝑜 1 𝑜 n 1 𝑜 1 𝑜
15 13 14 mtbiri n = 1 𝑜 ¬ 1 𝑜 n
16 15 con2i 1 𝑜 n ¬ n = 1 𝑜
17 16 intnanrd 1 𝑜 n ¬ n = 1 𝑜 x U
18 17 iffalsed 1 𝑜 n if n = 1 𝑜 x U if x V × U n 1 st x n x = if x V × U n 1 st x n x
19 18 adantl n ω 1 𝑜 n if n = 1 𝑜 x U if x V × U n 1 st x n x = if x V × U n 1 st x n x
20 iffalse ¬ x V × U if x V × U n 1 st x n x = n x
21 19 20 sylan9eq n ω 1 𝑜 n ¬ x V × U if n = 1 𝑜 x U if x V × U n 1 st x n x = n x
22 11 21 eqtrd n ω 1 𝑜 n ¬ x V × U n F x = n x
23 2 22 eqtr3id n ω 1 𝑜 n ¬ x V × U F n x = n x
24 23 ex n ω 1 𝑜 n ¬ x V × U F n x = n x