Theorem gonan0

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

	Ref	Expression
Assertion	gonan0	⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	neii	⊢ ¬ 1o = ∅
3	2	intnanr	⊢ ¬ ( 1o = ∅ ∧ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ )
4		1oex	⊢ 1o ∈ V
5		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
6	4 5	opth	⊢ ( ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ( 1o = ∅ ∧ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ) )
7	3 6	mtbir	⊢ ¬ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩
8		goel	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
9	8	eqeq2d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) ↔ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
10	7 9	mtbiri	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ¬ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) )
11	10	rgen2	⊢ ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 )
12		ralnex2	⊢ ( ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) ↔ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) )
13	11 12	mpbi	⊢ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 )
14	13	intnan	⊢ ¬ ( ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) )
15		eqeq1	⊢ ( 𝑥 = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) ) )
16	15	2rexbidv	⊢ ( 𝑥 = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) ) )
17		fmla0	⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
18	16 17	elrab2	⊢ ( ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ ( Fmla ‘ ∅ ) ↔ ( ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ = ( 𝑖 ∈𝑔 𝑗 ) ) )
19	14 18	mtbir	⊢ ¬ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ ( Fmla ‘ ∅ )
20		gonafv	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊼𝑔 𝐵 ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
21	20	eleq1d	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ↔ ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ ( Fmla ‘ ∅ ) ) )
22	19 21	mtbiri	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) )
23		eqid	⊢ ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ ) = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
24	23	dmmptss	⊢ dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ ) ⊆ ( V × V )
25		relxp	⊢ Rel ( V × V )
26		relss	⊢ ( dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ ) ⊆ ( V × V ) → ( Rel ( V × V ) → Rel dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ ) ) )
27	24 25 26	mp2	⊢ Rel dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
28		df-gona	⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
29	28	dmeqi	⊢ dom ⊼𝑔 = dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
30	29	releqi	⊢ ( Rel dom ⊼𝑔 ↔ Rel dom ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ ) )
31	27 30	mpbir	⊢ Rel dom ⊼𝑔
32	31	ovprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊼𝑔 𝐵 ) = ∅ )
33		peano1	⊢ ∅ ∈ ω
34		fmlaomn0	⊢ ( ∅ ∈ ω → ∅ ∉ ( Fmla ‘ ∅ ) )
35	33 34	ax-mp	⊢ ∅ ∉ ( Fmla ‘ ∅ )
36	35	neli	⊢ ¬ ∅ ∈ ( Fmla ‘ ∅ )
37		eleq1	⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) = ∅ → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ↔ ∅ ∈ ( Fmla ‘ ∅ ) ) )
38	36 37	mtbiri	⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) = ∅ → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) )
39	32 38	syl	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) )
40	22 39	pm2.61i	⊢ ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ )
41		fveq2	⊢ ( 𝑁 = ∅ → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ ∅ ) )
42	41	eleq2d	⊢ ( 𝑁 = ∅ → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) ↔ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) )
43	40 42	mtbiri	⊢ ( 𝑁 = ∅ → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) )
44	43	necon2ai	⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ )