This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑁 ) → 𝑁 ≠ ∅ )