Metamath Proof Explorer

Theorem gonarlem

Description: Lemma for gonar (induction step). (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion gonarlem ${⊢}{N}\in \mathrm{\omega }\to \left(\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 peano2 ${⊢}{N}\in \mathrm{\omega }\to \mathrm{suc}{N}\in \mathrm{\omega }$
2 ovexd ${⊢}{N}\in \mathrm{\omega }\to {a}{⊼}_{𝑔}{b}\in \mathrm{V}$
3 isfmlasuc ${⊢}\left(\mathrm{suc}{N}\in \mathrm{\omega }\wedge {a}{⊼}_{𝑔}{b}\in \mathrm{V}\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)↔\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\vee \exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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)$
4 1 2 3 syl2anc ${⊢}{N}\in \mathrm{\omega }\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)↔\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\vee \exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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)$
5 4 adantr ${⊢}\left({N}\in \mathrm{\omega }\wedge \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)↔\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\vee \exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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)$
6 fmlasssuc ${⊢}\mathrm{suc}{N}\in \mathrm{\omega }\to \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\subseteq \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)$
7 1 6 syl ${⊢}{N}\in \mathrm{\omega }\to \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\subseteq \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)$
8 7 sseld ${⊢}{N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to {a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)$
9 7 sseld ${⊢}{N}\in \mathrm{\omega }\to \left({b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)$
10 8 9 anim12d ${⊢}{N}\in \mathrm{\omega }\to \left(\left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
11 10 com12 ${⊢}\left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
12 11 imim2i ${⊢}\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
13 12 com23 ${⊢}\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\to \left({N}\in \mathrm{\omega }\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
14 13 impcom ${⊢}\left({N}\in \mathrm{\omega }\wedge \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
15 gonafv ${⊢}\left({a}\in \mathrm{V}\wedge {b}\in \mathrm{V}\right)\to {a}{⊼}_{𝑔}{b}=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
16 15 el2v ${⊢}{a}{⊼}_{𝑔}{b}=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
17 16 a1i ${⊢}\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to {a}{⊼}_{𝑔}{b}=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
18 gonafv ${⊢}\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to {u}{⊼}_{𝑔}{v}=⟨{1}_{𝑜},⟨{u},{v}⟩⟩$
19 17 18 eqeq12d ${⊢}\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({a}{⊼}_{𝑔}{b}={u}{⊼}_{𝑔}{v}↔⟨{1}_{𝑜},⟨{a},{b}⟩⟩=⟨{1}_{𝑜},⟨{u},{v}⟩⟩\right)$
20 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
21 opex ${⊢}⟨{a},{b}⟩\in \mathrm{V}$
22 20 21 opth ${⊢}⟨{1}_{𝑜},⟨{a},{b}⟩⟩=⟨{1}_{𝑜},⟨{u},{v}⟩⟩↔\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)$
23 19 22 syl6bb ${⊢}\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({a}{⊼}_{𝑔}{b}={u}{⊼}_{𝑔}{v}↔\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)\right)$
24 23 adantll ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({a}{⊼}_{𝑔}{b}={u}{⊼}_{𝑔}{v}↔\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)\right)$
25 vex ${⊢}{a}\in \mathrm{V}$
26 vex ${⊢}{b}\in \mathrm{V}$
27 25 26 opth ${⊢}⟨{a},{b}⟩=⟨{u},{v}⟩↔\left({a}={u}\wedge {b}={v}\right)$
28 eleq1w ${⊢}{u}={a}\to \left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔{a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
29 28 equcoms ${⊢}{a}={u}\to \left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔{a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
30 eleq1w ${⊢}{v}={b}\to \left({v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
31 30 equcoms ${⊢}{b}={v}\to \left({v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
32 29 31 bi2anan9 ${⊢}\left({a}={u}\wedge {b}={v}\right)\to \left(\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)↔\left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)$
33 32 11 syl6bi ${⊢}\left({a}={u}\wedge {b}={v}\right)\to \left(\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
34 27 33 sylbi ${⊢}⟨{a},{b}⟩=⟨{u},{v}⟩\to \left(\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
35 34 adantl ${⊢}\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)\to \left(\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({N}\in \mathrm{\omega }\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
36 35 com13 ${⊢}{N}\in \mathrm{\omega }\to \left(\left({u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left(\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$
37 36 impl ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left(\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{a},{b}⟩=⟨{u},{v}⟩\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
38 24 37 sylbid ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({a}{⊼}_{𝑔}{b}={u}{⊼}_{𝑔}{v}\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
39 38 rexlimdva ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{a}{⊼}_{𝑔}{b}={u}{⊼}_{𝑔}{v}\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
40 gonanegoal ${⊢}{a}{⊼}_{𝑔}{b}\ne \left[{\forall }_{𝑔}{i}{u}\right]$
41 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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
42 40 41 mpi ${⊢}{a}{⊼}_{𝑔}{b}=\left[{\forall }_{𝑔}{i}{u}\right]\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)$
43 42 a1i ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
44 43 rexlimdva ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
45 39 44 jaod ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left(\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
46 45 rexlimdva ${⊢}{N}\in \mathrm{\omega }\to \left(\exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
47 46 adantr ${⊢}\left({N}\in \mathrm{\omega }\wedge \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\right)\to \left(\exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
48 14 47 jaod ${⊢}\left({N}\in \mathrm{\omega }\wedge \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\right)\to \left(\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\vee \exists {u}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\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}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
49 5 48 sylbid ${⊢}\left({N}\in \mathrm{\omega }\wedge \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)$
50 49 ex ${⊢}{N}\in \mathrm{\omega }\to \left(\left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)\to \left({a}{⊼}_{𝑔}{b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\to \left({a}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\wedge {b}\in \mathrm{Fmla}\left(\mathrm{suc}\mathrm{suc}{N}\right)\right)\right)\right)$