Metamath Proof Explorer


Theorem goalr

Description: If the "Godel-set of universal quantification" applied to a class is a Godel formula, the class is also a Godel formula. Remark: The reverse is not valid for A being of the same height as the "Godel-set of universal quantification". (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goalr N ω 𝑔 i a Fmla N a Fmla N

Proof

Step Hyp Ref Expression
1 goaln0 𝑔 i a Fmla N N
2 1 adantl N ω 𝑔 i a Fmla N N
3 nnsuc N ω N n ω N = suc n
4 suceq x = suc x = suc
5 4 fveq2d x = Fmla suc x = Fmla suc
6 5 eleq2d x = 𝑔 i a Fmla suc x 𝑔 i a Fmla suc
7 5 eleq2d x = a Fmla suc x a Fmla suc
8 6 7 imbi12d x = 𝑔 i a Fmla suc x a Fmla suc x 𝑔 i a Fmla suc a Fmla suc
9 suceq x = y suc x = suc y
10 9 fveq2d x = y Fmla suc x = Fmla suc y
11 10 eleq2d x = y 𝑔 i a Fmla suc x 𝑔 i a Fmla suc y
12 10 eleq2d x = y a Fmla suc x a Fmla suc y
13 11 12 imbi12d x = y 𝑔 i a Fmla suc x a Fmla suc x 𝑔 i a Fmla suc y a Fmla suc y
14 suceq x = suc y suc x = suc suc y
15 14 fveq2d x = suc y Fmla suc x = Fmla suc suc y
16 15 eleq2d x = suc y 𝑔 i a Fmla suc x 𝑔 i a Fmla suc suc y
17 15 eleq2d x = suc y a Fmla suc x a Fmla suc suc y
18 16 17 imbi12d x = suc y 𝑔 i a Fmla suc x a Fmla suc x 𝑔 i a Fmla suc suc y a Fmla suc suc y
19 suceq x = n suc x = suc n
20 19 fveq2d x = n Fmla suc x = Fmla suc n
21 20 eleq2d x = n 𝑔 i a Fmla suc x 𝑔 i a Fmla suc n
22 20 eleq2d x = n a Fmla suc x a Fmla suc n
23 21 22 imbi12d x = n 𝑔 i a Fmla suc x a Fmla suc x 𝑔 i a Fmla suc n a Fmla suc n
24 peano1 ω
25 df-goal 𝑔 i a = 2 𝑜 i a
26 opex 2 𝑜 i a V
27 25 26 eqeltri 𝑔 i a V
28 isfmlasuc ω 𝑔 i a V 𝑔 i a Fmla suc 𝑔 i a Fmla u Fmla v Fmla 𝑔 i a = u 𝑔 v k ω 𝑔 i a = 𝑔 k u
29 24 27 28 mp2an 𝑔 i a Fmla suc 𝑔 i a Fmla u Fmla v Fmla 𝑔 i a = u 𝑔 v k ω 𝑔 i a = 𝑔 k u
30 eqeq1 x = 𝑔 i a x = k 𝑔 j 𝑔 i a = k 𝑔 j
31 30 2rexbidv x = 𝑔 i a k ω j ω x = k 𝑔 j k ω j ω 𝑔 i a = k 𝑔 j
32 fmla0 Fmla = x V | k ω j ω x = k 𝑔 j
33 31 32 elrab2 𝑔 i a Fmla 𝑔 i a V k ω j ω 𝑔 i a = k 𝑔 j
34 25 a1i k ω j ω 𝑔 i a = 2 𝑜 i a
35 goel k ω j ω k 𝑔 j = k j
36 34 35 eqeq12d k ω j ω 𝑔 i a = k 𝑔 j 2 𝑜 i a = k j
37 2oex 2 𝑜 V
38 opex i a V
39 37 38 opth 2 𝑜 i a = k j 2 𝑜 = i a = k j
40 2on0 2 𝑜
41 eqneqall 2 𝑜 = 2 𝑜 a Fmla suc
42 40 41 mpi 2 𝑜 = a Fmla suc
43 42 adantr 2 𝑜 = i a = k j a Fmla suc
44 39 43 sylbi 2 𝑜 i a = k j a Fmla suc
45 36 44 syl6bi k ω j ω 𝑔 i a = k 𝑔 j a Fmla suc
46 45 rexlimdva k ω j ω 𝑔 i a = k 𝑔 j a Fmla suc
47 46 rexlimiv k ω j ω 𝑔 i a = k 𝑔 j a Fmla suc
48 33 47 simplbiim 𝑔 i a Fmla a Fmla suc
49 gonanegoal u 𝑔 v 𝑔 i a
50 eqneqall u 𝑔 v = 𝑔 i a u 𝑔 v 𝑔 i a a Fmla suc
51 49 50 mpi u 𝑔 v = 𝑔 i a a Fmla suc
52 51 eqcoms 𝑔 i a = u 𝑔 v a Fmla suc
53 52 a1i u Fmla v Fmla 𝑔 i a = u 𝑔 v a Fmla suc
54 53 rexlimdva u Fmla v Fmla 𝑔 i a = u 𝑔 v a Fmla suc
55 df-goal 𝑔 k u = 2 𝑜 k u
56 25 55 eqeq12i 𝑔 i a = 𝑔 k u 2 𝑜 i a = 2 𝑜 k u
57 37 38 opth 2 𝑜 i a = 2 𝑜 k u 2 𝑜 = 2 𝑜 i a = k u
58 vex i V
59 vex a V
60 58 59 opth i a = k u i = k a = u
61 eleq1w u = a u Fmla a Fmla
62 fmlasssuc ω Fmla Fmla suc
63 24 62 ax-mp Fmla Fmla suc
64 63 sseli a Fmla a Fmla suc
65 61 64 syl6bi u = a u Fmla a Fmla suc
66 65 eqcoms a = u u Fmla a Fmla suc
67 60 66 simplbiim i a = k u u Fmla a Fmla suc
68 57 67 simplbiim 2 𝑜 i a = 2 𝑜 k u u Fmla a Fmla suc
69 68 com12 u Fmla 2 𝑜 i a = 2 𝑜 k u a Fmla suc
70 69 adantr u Fmla k ω 2 𝑜 i a = 2 𝑜 k u a Fmla suc
71 56 70 syl5bi u Fmla k ω 𝑔 i a = 𝑔 k u a Fmla suc
72 71 rexlimdva u Fmla k ω 𝑔 i a = 𝑔 k u a Fmla suc
73 54 72 jaod u Fmla v Fmla 𝑔 i a = u 𝑔 v k ω 𝑔 i a = 𝑔 k u a Fmla suc
74 73 rexlimiv u Fmla v Fmla 𝑔 i a = u 𝑔 v k ω 𝑔 i a = 𝑔 k u a Fmla suc
75 48 74 jaoi 𝑔 i a Fmla u Fmla v Fmla 𝑔 i a = u 𝑔 v k ω 𝑔 i a = 𝑔 k u a Fmla suc
76 29 75 sylbi 𝑔 i a Fmla suc a Fmla suc
77 goalrlem y ω 𝑔 i a Fmla suc y a Fmla suc y 𝑔 i a Fmla suc suc y a Fmla suc suc y
78 8 13 18 23 76 77 finds n ω 𝑔 i a Fmla suc n a Fmla suc n
79 78 adantr n ω N = suc n 𝑔 i a Fmla suc n a Fmla suc n
80 fveq2 N = suc n Fmla N = Fmla suc n
81 80 eleq2d N = suc n 𝑔 i a Fmla N 𝑔 i a Fmla suc n
82 80 eleq2d N = suc n a Fmla N a Fmla suc n
83 81 82 imbi12d N = suc n 𝑔 i a Fmla N a Fmla N 𝑔 i a Fmla suc n a Fmla suc n
84 83 adantl n ω N = suc n 𝑔 i a Fmla N a Fmla N 𝑔 i a Fmla suc n a Fmla suc n
85 79 84 mpbird n ω N = suc n 𝑔 i a Fmla N a Fmla N
86 85 rexlimiva n ω N = suc n 𝑔 i a Fmla N a Fmla N
87 3 86 syl N ω N 𝑔 i a Fmla N a Fmla N
88 87 impancom N ω 𝑔 i a Fmla N N a Fmla N
89 2 88 mpd N ω 𝑔 i a Fmla N a Fmla N