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