# 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 ${⊢}\left({N}\in \mathrm{\omega }\wedge {a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left({N}\right)\right)\to \left({a}\in \mathrm{Fmla}\left({N}\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)$

### Proof

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