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

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