Metamath Proof Explorer


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