Metamath Proof Explorer

Theorem gonar

Description: If the "Godel-set of NAND" applied to classes is a Godel formula, the classes are also Godel formulas. Remark: The reverse is not valid for A or B being of the same height as the "Godel-set of NAND". (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion gonar ⊢N∈ω∧a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N

Proof

Step Hyp Ref Expression
1 gonan0 ⊢a⊼𝑔b∈Fmla⁡N→N≠∅
2 1 adantl ⊢N∈ω∧a⊼𝑔b∈Fmla⁡N→N≠∅
3 nnsuc ⊢N∈ω∧N≠∅→∃x∈ωN=suc⁡x
4 suceq ⊢d=∅→suc⁡d=suc⁡∅
5 4 fveq2d ⊢d=∅→Fmla⁡suc⁡d=Fmla⁡suc⁡∅
6 5 eleq2d ⊢d=∅→a⊼𝑔b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡∅
7 5 eleq2d ⊢d=∅→a∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡∅
8 5 eleq2d ⊢d=∅→b∈Fmla⁡suc⁡d↔b∈Fmla⁡suc⁡∅
9 7 8 anbi12d ⊢d=∅→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
10 6 9 imbi12d ⊢d=∅→a⊼𝑔b∈Fmla⁡suc⁡d→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
11 suceq ⊢d=c→suc⁡d=suc⁡c
12 11 fveq2d ⊢d=c→Fmla⁡suc⁡d=Fmla⁡suc⁡c
13 12 eleq2d ⊢d=c→a⊼𝑔b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡c
14 12 eleq2d ⊢d=c→a∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡c
15 12 eleq2d ⊢d=c→b∈Fmla⁡suc⁡d↔b∈Fmla⁡suc⁡c
16 14 15 anbi12d ⊢d=c→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡c∧b∈Fmla⁡suc⁡c
17 13 16 imbi12d ⊢d=c→a⊼𝑔b∈Fmla⁡suc⁡d→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡c→a∈Fmla⁡suc⁡c∧b∈Fmla⁡suc⁡c
18 suceq ⊢d=suc⁡c→suc⁡d=suc⁡suc⁡c
19 18 fveq2d ⊢d=suc⁡c→Fmla⁡suc⁡d=Fmla⁡suc⁡suc⁡c
20 19 eleq2d ⊢d=suc⁡c→a⊼𝑔b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡suc⁡c
21 19 eleq2d ⊢d=suc⁡c→a∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡suc⁡c
22 19 eleq2d ⊢d=suc⁡c→b∈Fmla⁡suc⁡d↔b∈Fmla⁡suc⁡suc⁡c
23 21 22 anbi12d ⊢d=suc⁡c→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡suc⁡c∧b∈Fmla⁡suc⁡suc⁡c
24 20 23 imbi12d ⊢d=suc⁡c→a⊼𝑔b∈Fmla⁡suc⁡d→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡suc⁡c→a∈Fmla⁡suc⁡suc⁡c∧b∈Fmla⁡suc⁡suc⁡c
25 suceq ⊢d=x→suc⁡d=suc⁡x
26 25 fveq2d ⊢d=x→Fmla⁡suc⁡d=Fmla⁡suc⁡x
27 26 eleq2d ⊢d=x→a⊼𝑔b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡x
28 26 eleq2d ⊢d=x→a∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡x
29 26 eleq2d ⊢d=x→b∈Fmla⁡suc⁡d↔b∈Fmla⁡suc⁡x
30 28 29 anbi12d ⊢d=x→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
31 27 30 imbi12d ⊢d=x→a⊼𝑔b∈Fmla⁡suc⁡d→a∈Fmla⁡suc⁡d∧b∈Fmla⁡suc⁡d↔a⊼𝑔b∈Fmla⁡suc⁡x→a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
32 peano1 ⊢∅∈ω
33 ovex ⊢a⊼𝑔b∈V
34 isfmlasuc ⊢∅∈ω∧a⊼𝑔b∈V→a⊼𝑔b∈Fmla⁡suc⁡∅↔a⊼𝑔b∈Fmla⁡∅∨∃u∈Fmla⁡∅∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v∨∃i∈ωa⊼𝑔b=∀𝑔iu
35 32 33 34 mp2an ⊢a⊼𝑔b∈Fmla⁡suc⁡∅↔a⊼𝑔b∈Fmla⁡∅∨∃u∈Fmla⁡∅∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v∨∃i∈ωa⊼𝑔b=∀𝑔iu
36 eqeq1 ⊢x=a⊼𝑔b→x=i∈𝑔j↔a⊼𝑔b=i∈𝑔j
37 36 2rexbidv ⊢x=a⊼𝑔b→∃i∈ω∃j∈ωx=i∈𝑔j↔∃i∈ω∃j∈ωa⊼𝑔b=i∈𝑔j
38 fmla0 ⊢Fmla⁡∅=x∈V|∃i∈ω∃j∈ωx=i∈𝑔j
39 37 38 elrab2 ⊢a⊼𝑔b∈Fmla⁡∅↔a⊼𝑔b∈V∧∃i∈ω∃j∈ωa⊼𝑔b=i∈𝑔j
40 gonafv ⊢a∈V∧b∈V→a⊼𝑔b=1𝑜ab
41 40 el2v ⊢a⊼𝑔b=1𝑜ab
42 41 a1i ⊢i∈ω∧j∈ω→a⊼𝑔b=1𝑜ab
43 goel ⊢i∈ω∧j∈ω→i∈𝑔j=∅ij
44 42 43 eqeq12d ⊢i∈ω∧j∈ω→a⊼𝑔b=i∈𝑔j↔1𝑜ab=∅ij
45 1oex ⊢1𝑜∈V
46 opex ⊢ab∈V
47 45 46 opth ⊢1𝑜ab=∅ij↔1𝑜=∅∧ab=ij
48 1n0 ⊢1𝑜≠∅
49 eqneqall ⊢1𝑜=∅→1𝑜≠∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
50 48 49 mpi ⊢1𝑜=∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
51 50 adantr ⊢1𝑜=∅∧ab=ij→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
52 47 51 sylbi ⊢1𝑜ab=∅ij→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
53 44 52 syl6bi ⊢i∈ω∧j∈ω→a⊼𝑔b=i∈𝑔j→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
54 53 rexlimdva ⊢i∈ω→∃j∈ωa⊼𝑔b=i∈𝑔j→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
55 54 rexlimiv ⊢∃i∈ω∃j∈ωa⊼𝑔b=i∈𝑔j→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
56 55 adantl ⊢a⊼𝑔b∈V∧∃i∈ω∃j∈ωa⊼𝑔b=i∈𝑔j→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
57 39 56 sylbi ⊢a⊼𝑔b∈Fmla⁡∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
58 41 a1i ⊢u∈Fmla⁡∅∧v∈Fmla⁡∅→a⊼𝑔b=1𝑜ab
59 gonafv ⊢u∈Fmla⁡∅∧v∈Fmla⁡∅→u⊼𝑔v=1𝑜uv
60 58 59 eqeq12d ⊢u∈Fmla⁡∅∧v∈Fmla⁡∅→a⊼𝑔b=u⊼𝑔v↔1𝑜ab=1𝑜uv
61 45 46 opth ⊢1𝑜ab=1𝑜uv↔1𝑜=1𝑜∧ab=uv
62 vex ⊢a∈V
63 vex ⊢b∈V
64 62 63 opth ⊢ab=uv↔a=u∧b=v
65 simpl ⊢a=u∧b=v→a=u
66 65 equcomd ⊢a=u∧b=v→u=a
67 66 eleq1d ⊢a=u∧b=v→u∈Fmla⁡∅↔a∈Fmla⁡∅
68 simpr ⊢a=u∧b=v→b=v
69 68 equcomd ⊢a=u∧b=v→v=b
70 69 eleq1d ⊢a=u∧b=v→v∈Fmla⁡∅↔b∈Fmla⁡∅
71 67 70 anbi12d ⊢a=u∧b=v→u∈Fmla⁡∅∧v∈Fmla⁡∅↔a∈Fmla⁡∅∧b∈Fmla⁡∅
72 64 71 sylbi ⊢ab=uv→u∈Fmla⁡∅∧v∈Fmla⁡∅↔a∈Fmla⁡∅∧b∈Fmla⁡∅
73 72 adantl ⊢1𝑜=1𝑜∧ab=uv→u∈Fmla⁡∅∧v∈Fmla⁡∅↔a∈Fmla⁡∅∧b∈Fmla⁡∅
74 61 73 sylbi ⊢1𝑜ab=1𝑜uv→u∈Fmla⁡∅∧v∈Fmla⁡∅↔a∈Fmla⁡∅∧b∈Fmla⁡∅
75 fmlasssuc ⊢∅∈ω→Fmla⁡∅⊆Fmla⁡suc⁡∅
76 32 75 ax-mp ⊢Fmla⁡∅⊆Fmla⁡suc⁡∅
77 76 sseli ⊢a∈Fmla⁡∅→a∈Fmla⁡suc⁡∅
78 76 sseli ⊢b∈Fmla⁡∅→b∈Fmla⁡suc⁡∅
79 77 78 anim12i ⊢a∈Fmla⁡∅∧b∈Fmla⁡∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
80 74 79 syl6bi ⊢1𝑜ab=1𝑜uv→u∈Fmla⁡∅∧v∈Fmla⁡∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
81 80 com12 ⊢u∈Fmla⁡∅∧v∈Fmla⁡∅→1𝑜ab=1𝑜uv→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
82 60 81 sylbid ⊢u∈Fmla⁡∅∧v∈Fmla⁡∅→a⊼𝑔b=u⊼𝑔v→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
83 82 rexlimdva ⊢u∈Fmla⁡∅→∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
84 gonanegoal ⊢a⊼𝑔b≠∀𝑔iu
85 eqneqall ⊢a⊼𝑔b=∀𝑔iu→a⊼𝑔b≠∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
86 84 85 mpi ⊢a⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
87 86 a1i ⊢u∈Fmla⁡∅∧i∈ω→a⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
88 87 rexlimdva ⊢u∈Fmla⁡∅→∃i∈ωa⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
89 83 88 jaod ⊢u∈Fmla⁡∅→∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v∨∃i∈ωa⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
90 89 rexlimiv ⊢∃u∈Fmla⁡∅∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v∨∃i∈ωa⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
91 57 90 jaoi ⊢a⊼𝑔b∈Fmla⁡∅∨∃u∈Fmla⁡∅∃v∈Fmla⁡∅a⊼𝑔b=u⊼𝑔v∨∃i∈ωa⊼𝑔b=∀𝑔iu→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
92 35 91 sylbi ⊢a⊼𝑔b∈Fmla⁡suc⁡∅→a∈Fmla⁡suc⁡∅∧b∈Fmla⁡suc⁡∅
93 gonarlem ⊢c∈ω→a⊼𝑔b∈Fmla⁡suc⁡c→a∈Fmla⁡suc⁡c∧b∈Fmla⁡suc⁡c→a⊼𝑔b∈Fmla⁡suc⁡suc⁡c→a∈Fmla⁡suc⁡suc⁡c∧b∈Fmla⁡suc⁡suc⁡c
94 10 17 24 31 92 93 finds ⊢x∈ω→a⊼𝑔b∈Fmla⁡suc⁡x→a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
95 94 adantr ⊢x∈ω∧N=suc⁡x→a⊼𝑔b∈Fmla⁡suc⁡x→a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
96 fveq2 ⊢N=suc⁡x→Fmla⁡N=Fmla⁡suc⁡x
97 96 eleq2d ⊢N=suc⁡x→a⊼𝑔b∈Fmla⁡N↔a⊼𝑔b∈Fmla⁡suc⁡x
98 96 eleq2d ⊢N=suc⁡x→a∈Fmla⁡N↔a∈Fmla⁡suc⁡x
99 96 eleq2d ⊢N=suc⁡x→b∈Fmla⁡N↔b∈Fmla⁡suc⁡x
100 98 99 anbi12d ⊢N=suc⁡x→a∈Fmla⁡N∧b∈Fmla⁡N↔a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
101 97 100 imbi12d ⊢N=suc⁡x→a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N↔a⊼𝑔b∈Fmla⁡suc⁡x→a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
102 101 adantl ⊢x∈ω∧N=suc⁡x→a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N↔a⊼𝑔b∈Fmla⁡suc⁡x→a∈Fmla⁡suc⁡x∧b∈Fmla⁡suc⁡x
103 95 102 mpbird ⊢x∈ω∧N=suc⁡x→a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N
104 103 rexlimiva ⊢∃x∈ωN=suc⁡x→a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N
105 3 104 syl ⊢N∈ω∧N≠∅→a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N
106 105 impancom ⊢N∈ω∧a⊼𝑔b∈Fmla⁡N→N≠∅→a∈Fmla⁡N∧b∈Fmla⁡N
107 2 106 mpd ⊢N∈ω∧a⊼𝑔b∈Fmla⁡N→a∈Fmla⁡N∧b∈Fmla⁡N