Metamath Proof Explorer


Theorem goaln0

Description: The "Godel-set of universal quantification" is a Godel formula of at least height 1. (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goaln0 ( ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 df-goal 𝑔 𝑖 𝐴 = ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩
2 2on0 2o ≠ ∅
3 2 neii ¬ 2o = ∅
4 3 intnanr ¬ ( 2o = ∅ ∧ ⟨ 𝑖 , 𝐴 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ )
5 2oex 2o ∈ V
6 opex 𝑖 , 𝐴 ⟩ ∈ V
7 5 6 opth ( ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ↔ ( 2o = ∅ ∧ ⟨ 𝑖 , 𝐴 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) )
8 4 7 mtbir ¬ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩
9 goel ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑘𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ )
10 9 eqeq2d ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ( ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) ↔ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑘 , 𝑗 ⟩ ⟩ ) )
11 8 10 mtbiri ( ( 𝑘 ∈ ω ∧ 𝑗 ∈ ω ) → ¬ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) )
12 11 rgen2 𝑘 ∈ ω ∀ 𝑗 ∈ ω ¬ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 )
13 ralnex2 ( ∀ 𝑘 ∈ ω ∀ 𝑗 ∈ ω ¬ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) ↔ ¬ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) )
14 12 13 mpbi ¬ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 )
15 14 intnan ¬ ( ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ ∈ V ∧ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) )
16 eqeq1 ( 𝑥 = ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ → ( 𝑥 = ( 𝑘𝑔 𝑗 ) ↔ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) ) )
17 16 2rexbidv ( 𝑥 = ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ → ( ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘𝑔 𝑗 ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) ) )
18 fmla0 ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑘𝑔 𝑗 ) }
19 17 18 elrab2 ( ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ ∈ ( Fmla ‘ ∅ ) ↔ ( ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ ∈ V ∧ ∃ 𝑘 ∈ ω ∃ 𝑗 ∈ ω ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ = ( 𝑘𝑔 𝑗 ) ) )
20 15 19 mtbir ¬ ⟨ 2o , ⟨ 𝑖 , 𝐴 ⟩ ⟩ ∈ ( Fmla ‘ ∅ )
21 1 20 eqneltri ¬ ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ ∅ )
22 fveq2 ( 𝑁 = ∅ → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ ∅ ) )
23 22 eleq2d ( 𝑁 = ∅ → ( ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ 𝑁 ) ↔ ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ ∅ ) ) )
24 21 23 mtbiri ( 𝑁 = ∅ → ¬ ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ 𝑁 ) )
25 24 necon2ai ( ∀𝑔 𝑖 𝐴 ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )