Metamath Proof Explorer


Theorem finxpreclem2

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

Ref Expression
Assertion finxpreclem2 X V ¬ X U ¬ = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X

Proof

Step Hyp Ref Expression
1 nfv x X V ¬ X U
2 nfmpo2 _ x n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
3 nfcv _ x 1 𝑜 X
4 2 3 nffv _ x n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
5 nfcv _ x
6 4 5 nfne x n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
7 1 6 nfim x X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
8 nfv n x = X
9 nfv n X V ¬ X U
10 nfmpo1 _ n n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
11 nfcv _ n 1 𝑜 X
12 10 11 nffv _ n n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
13 nfcv _ n
14 12 13 nfne n n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
15 9 14 nfim n X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
16 8 15 nfim n x = X X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
17 1onn 1 𝑜 ω
18 17 elexi 1 𝑜 V
19 df-ov 1 𝑜 n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x X = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
20 0ex V
21 opex n 1 st x V
22 opex n x V
23 21 22 ifex if x V × U n 1 st x n x V
24 20 23 ifex if n = 1 𝑜 x U if x V × U n 1 st x n x V
25 24 csbex X / x if n = 1 𝑜 x U if x V × U n 1 st x n x V
26 25 csbex 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x V
27 eqid n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
28 27 ovmpos 1 𝑜 ω X V 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x V 1 𝑜 n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x X = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
29 17 26 28 mp3an13 X V 1 𝑜 n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x X = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
30 29 adantr X V ¬ X U n = 1 𝑜 x = X 1 𝑜 n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x X = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
31 csbeq1a x = X if n = 1 𝑜 x U if x V × U n 1 st x n x = X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
32 csbeq1a n = 1 𝑜 X / x if n = 1 𝑜 x U if x V × U n 1 st x n x = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
33 31 32 sylan9eqr n = 1 𝑜 x = X if n = 1 𝑜 x U if x V × U n 1 st x n x = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
34 33 adantl ¬ X U n = 1 𝑜 x = X if n = 1 𝑜 x U if x V × U n 1 st x n x = 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
35 eleq1 x = X x U X U
36 35 notbid x = X ¬ x U ¬ X U
37 36 biimprcd ¬ X U x = X ¬ x U
38 pm3.14 ¬ n = 1 𝑜 ¬ x U ¬ n = 1 𝑜 x U
39 38 olcs ¬ x U ¬ n = 1 𝑜 x U
40 37 39 syl6 ¬ X U x = X ¬ n = 1 𝑜 x U
41 iffalse ¬ n = 1 𝑜 x U 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
42 40 41 syl6 ¬ X U x = X 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
43 42 imp ¬ X U x = X 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
44 ifeqor if x V × U n 1 st x n x = n 1 st x if x V × U n 1 st x n x = n x
45 vuniex n V
46 fvex 1 st x V
47 45 46 opnzi n 1 st x
48 47 neii ¬ n 1 st x =
49 eqeq1 if x V × U n 1 st x n x = n 1 st x if x V × U n 1 st x n x = n 1 st x =
50 48 49 mtbiri if x V × U n 1 st x n x = n 1 st x ¬ if x V × U n 1 st x n x =
51 vex n V
52 vex x V
53 51 52 opnzi n x
54 53 neii ¬ n x =
55 eqeq1 if x V × U n 1 st x n x = n x if x V × U n 1 st x n x = n x =
56 54 55 mtbiri if x V × U n 1 st x n x = n x ¬ if x V × U n 1 st x n x =
57 50 56 jaoi if x V × U n 1 st x n x = n 1 st x if x V × U n 1 st x n x = n x ¬ if x V × U n 1 st x n x =
58 44 57 mp1i ¬ X U x = X ¬ if x V × U n 1 st x n x =
59 58 neqned ¬ X U x = X if x V × U n 1 st x n x
60 43 59 eqnetrd ¬ X U x = X if n = 1 𝑜 x U if x V × U n 1 st x n x
61 60 adantrl ¬ X U n = 1 𝑜 x = X if n = 1 𝑜 x U if x V × U n 1 st x n x
62 34 61 eqnetrrd ¬ X U n = 1 𝑜 x = X 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
63 62 adantl X V ¬ X U n = 1 𝑜 x = X 1 𝑜 / n X / x if n = 1 𝑜 x U if x V × U n 1 st x n x
64 30 63 eqnetrd X V ¬ X U n = 1 𝑜 x = X 1 𝑜 n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x X
65 19 64 eqnetrrid X V ¬ X U n = 1 𝑜 x = X n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
66 65 ancom2s X V n = 1 𝑜 x = X ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
67 66 an12s n = 1 𝑜 x = X X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
68 67 exp31 n = 1 𝑜 x = X X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
69 16 18 68 vtoclef x = X X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
70 7 69 vtoclefex X V X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
71 70 anabsi5 X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
72 71 necomd X V ¬ X U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X
73 72 neneqd X V ¬ X U ¬ = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 X