Metamath Proof Explorer


Theorem fmlasuc0

Description: The valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 18-Sep-2023)

Ref Expression
Assertion fmlasuc0 N ω Fmla suc N = Fmla N x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u

Proof

Step Hyp Ref Expression
1 df-fmla Fmla = n suc ω dom Sat n
2 fveq2 n = suc N Sat n = Sat suc N
3 2 dmeqd n = suc N dom Sat n = dom Sat suc N
4 omsucelsucb N ω suc N suc ω
5 4 biimpi N ω suc N suc ω
6 fvex Sat suc N V
7 6 dmex dom Sat suc N V
8 7 a1i N ω dom Sat suc N V
9 1 3 5 8 fvmptd3 N ω Fmla suc N = dom Sat suc N
10 satf0sucom suc N suc ω Sat suc N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N
11 5 10 syl N ω Sat suc N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N
12 nnon N ω N On
13 rdgsuc N On rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
14 12 13 syl N ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
15 11 14 eqtrd N ω Sat suc N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
16 15 dmeqd N ω dom Sat suc N = dom f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
17 elelsuc N ω N suc ω
18 satf0sucom N suc ω Sat N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
19 18 eqcomd N suc ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = Sat N
20 17 19 syl N ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = Sat N
21 20 fveq2d N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u Sat N
22 eqidd N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
23 id f = Sat N f = Sat N
24 rexeq f = Sat N v f x = 1 st u 𝑔 1 st v v Sat N x = 1 st u 𝑔 1 st v
25 24 orbi1d f = Sat N v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
26 25 rexeqbi1dv f = Sat N u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
27 26 anbi2d f = Sat N y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
28 27 opabbidv f = Sat N x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
29 23 28 uneq12d f = Sat N f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
30 29 adantl N ω f = Sat N f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
31 fvex Sat N V
32 31 a1i N ω Sat N V
33 peano1 ω
34 eleq1 y = y ω ω
35 33 34 mpbiri y = y ω
36 35 adantr y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y ω
37 36 pm4.71ri y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
38 37 opabbii x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x y | y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
39 omex ω V
40 id ω V ω V
41 unab x | v Sat N x = 1 st u 𝑔 1 st v x | i ω x = 𝑔 i 1 st u = x | v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
42 31 abrexex x | v Sat N x = 1 st u 𝑔 1 st v V
43 39 abrexex x | i ω x = 𝑔 i 1 st u V
44 42 43 unex x | v Sat N x = 1 st u 𝑔 1 st v x | i ω x = 𝑔 i 1 st u V
45 41 44 eqeltrri x | v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
46 45 a1i ω V y ω u Sat N x | v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
47 46 ralrimiva ω V y ω u Sat N x | v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
48 abrexex2g Sat N V u Sat N x | v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
49 31 47 48 sylancr ω V y ω x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
50 40 49 opabex3rd ω V x y | y ω u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
51 39 50 ax-mp x y | y ω u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
52 simpr y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
53 52 anim2i y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y ω u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
54 53 ssopab2i x y | y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y ω u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
55 51 54 ssexi x y | y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
56 55 a1i N ω x y | y ω y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
57 38 56 eqeltrid N ω x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
58 unexg Sat N V x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
59 31 57 58 sylancr N ω Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
60 22 30 32 59 fvmptd N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u Sat N = Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
61 21 60 eqtrd N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
62 61 dmeqd N ω dom f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = dom Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
63 dmun dom Sat N x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = dom Sat N dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
64 62 63 eqtrdi N ω dom f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = dom Sat N dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
65 fmlafv N suc ω Fmla N = dom Sat N
66 17 65 syl N ω Fmla N = dom Sat N
67 66 eqcomd N ω dom Sat N = Fmla N
68 dmopab dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x | y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
69 68 a1i N ω dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x | y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
70 0ex V
71 70 isseti y y =
72 19.41v y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
73 71 72 mpbiran y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
74 73 abbii x | y y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
75 69 74 eqtrdi N ω dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
76 67 75 uneq12d N ω dom Sat N dom x y | y = u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = Fmla N x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
77 64 76 eqtrd N ω dom f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = Fmla N x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
78 9 16 77 3eqtrd N ω Fmla suc N = Fmla N x | u Sat N v Sat N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u