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 ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 goaln0 ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )
2 1 adantl ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑁 ≠ ∅ )
3 nnsuc ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 )
4 suceq ( 𝑥 = ∅ → suc 𝑥 = suc ∅ )
5 4 fveq2d ( 𝑥 = ∅ → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc ∅ ) )
6 5 eleq2d ( 𝑥 = ∅ → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
7 5 eleq2d ( 𝑥 = ∅ → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
8 6 7 imbi12d ( 𝑥 = ∅ → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) ) )
9 suceq ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
10 9 fveq2d ( 𝑥 = 𝑦 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc 𝑦 ) )
11 10 eleq2d ( 𝑥 = 𝑦 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) )
12 10 eleq2d ( 𝑥 = 𝑦 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) )
13 11 12 imbi12d ( 𝑥 = 𝑦 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) ) )
14 suceq ( 𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦 )
15 14 fveq2d ( 𝑥 = suc 𝑦 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc suc 𝑦 ) )
16 15 eleq2d ( 𝑥 = suc 𝑦 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) )
17 15 eleq2d ( 𝑥 = suc 𝑦 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) )
18 16 17 imbi12d ( 𝑥 = suc 𝑦 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) ) )
19 suceq ( 𝑥 = 𝑛 → suc 𝑥 = suc 𝑛 )
20 19 fveq2d ( 𝑥 = 𝑛 → ( Fmla ‘ suc 𝑥 ) = ( Fmla ‘ suc 𝑛 ) )
21 20 eleq2d ( 𝑥 = 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
22 20 eleq2d ( 𝑥 = 𝑛 → ( 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
23 21 22 imbi12d ( 𝑥 = 𝑛 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑥 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
24 peano1 ∅ ∈ ω
25 df-goal 𝑔 𝑖 𝑎 = ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩
26 opex ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ ∈ V
27 25 26 eqeltri 𝑔 𝑖 𝑎 ∈ V
28 isfmlasuc ( ( ∅ ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ V ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) ) )
29 24 27 28 mp2an ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) )
30 eqeq1 ( 𝑥 = ∀𝑔 𝑖 𝑎 → ( 𝑥 = ( 𝑘𝑔 𝑗 ) ↔ ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) ) )
31 30 2rexbidv ( 𝑥 = ∀𝑔 𝑖 𝑎 → ( ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘𝑔 𝑗 ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) ) )
32 fmla0 ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘𝑔 𝑗 ) }
33 31 32 elrab2 ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ V ∧ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) ) )
34 25 a1i ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ∀𝑔 𝑖 𝑎 = ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ )
35 goel ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑘𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ )
36 34 35 eqeq12d ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) ↔ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ) )
37 2oex 2o ∈ V
38 opex 𝑖 , 𝑎 ⟩ ∈ V
39 37 38 opth ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ↔ ( 2o = ∅ ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) )
40 2on0 2o ≠ ∅
41 eqneqall ( 2o = ∅ → ( 2o ≠ ∅ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
42 40 41 mpi ( 2o = ∅ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
43 42 adantr ( ( 2o = ∅ ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
44 39 43 sylbi ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
45 36 44 syl6bi ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
46 45 rexlimdva ( 𝑘 ∈ ω → ( ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
47 46 rexlimiv ( ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ∀𝑔 𝑖 𝑎 = ( 𝑘𝑔 𝑗 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
48 33 47 simplbiim ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
49 gonanegoal ( 𝑢𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎
50 eqneqall ( ( 𝑢𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎 → ( ( 𝑢𝑔 𝑣 ) ≠ ∀𝑔 𝑖 𝑎𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
51 49 50 mpi ( ( 𝑢𝑔 𝑣 ) = ∀𝑔 𝑖 𝑎𝑎 ∈ ( Fmla ‘ suc ∅ ) )
52 51 eqcoms ( ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
53 52 a1i ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑣 ∈ ( Fmla ‘ ∅ ) ) → ( ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
54 53 rexlimdva ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
55 df-goal 𝑔 𝑘 𝑢 = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩
56 25 55 eqeq12i ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ↔ ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ )
57 37 38 opth ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ ↔ ( 2o = 2o ∧ ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ ) )
58 vex 𝑖 ∈ V
59 vex 𝑎 ∈ V
60 58 59 opth ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ ↔ ( 𝑖 = 𝑘𝑎 = 𝑢 ) )
61 eleq1w ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) ↔ 𝑎 ∈ ( Fmla ‘ ∅ ) ) )
62 fmlasssuc ( ∅ ∈ ω → ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ ) )
63 24 62 ax-mp ( Fmla ‘ ∅ ) ⊆ ( Fmla ‘ suc ∅ )
64 63 sseli ( 𝑎 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
65 61 64 syl6bi ( 𝑢 = 𝑎 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
66 65 eqcoms ( 𝑎 = 𝑢 → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
67 60 66 simplbiim ( ⟨ 𝑖 , 𝑎 ⟩ = ⟨ 𝑘 , 𝑢 ⟩ → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
68 57 67 simplbiim ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → ( 𝑢 ∈ ( Fmla ‘ ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
69 68 com12 ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
70 69 adantr ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑘 ∈ ω ) → ( ⟨ 2o , ⟨ 𝑖 , 𝑎 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑘 , 𝑢 ⟩ ⟩ → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
71 56 70 syl5bi ( ( 𝑢 ∈ ( Fmla ‘ ∅ ) ∧ 𝑘 ∈ ω ) → ( ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
72 71 rexlimdva ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
73 54 72 jaod ( 𝑢 ∈ ( Fmla ‘ ∅ ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) ) )
74 73 rexlimiv ( ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
75 48 74 jaoi ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ ∅ ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) ∀𝑔 𝑖 𝑎 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑘 ∈ ω ∀𝑔 𝑖 𝑎 = ∀𝑔 𝑘 𝑢 ) ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
76 29 75 sylbi ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc ∅ ) → 𝑎 ∈ ( Fmla ‘ suc ∅ ) )
77 goalrlem ( 𝑦 ∈ ω → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑦 ) ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) → 𝑎 ∈ ( Fmla ‘ suc suc 𝑦 ) ) ) )
78 8 13 18 23 76 77 finds ( 𝑛 ∈ ω → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
79 78 adantr ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
80 fveq2 ( 𝑁 = suc 𝑛 → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ suc 𝑛 ) )
81 80 eleq2d ( 𝑁 = suc 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ↔ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
82 80 eleq2d ( 𝑁 = suc 𝑛 → ( 𝑎 ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) )
83 81 82 imbi12d ( 𝑁 = suc 𝑛 → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
84 83 adantl ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) ↔ ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) → 𝑎 ∈ ( Fmla ‘ suc 𝑛 ) ) ) )
85 79 84 mpbird ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
86 85 rexlimiva ( ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
87 3 86 syl ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
88 87 impancom ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑁 ≠ ∅ → 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) )
89 2 88 mpd ( ( 𝑁 ∈ ω ∧ ∀𝑔 𝑖 𝑎 ∈ ( Fmla ‘ 𝑁 ) ) → 𝑎 ∈ ( Fmla ‘ 𝑁 ) )