# Metamath Proof Explorer

## Theorem fmlasucdisj

Description: The valid Godel formulas of height ( N + 1 ) is disjoint with the difference ( ( Fmlasuc suc N ) \ ( Fmlasuc N ) ) , expressed by formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification based on the valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 20-Oct-2023)

Ref Expression
Assertion fmlasucdisj ${⊢}{N}\in \mathrm{\omega }\to \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\cap \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}=\varnothing$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{f}\in \mathrm{V}$
2 eqeq1 ${⊢}{x}={f}\to \left({x}={u}{⊼}_{𝑔}{v}↔{f}={u}{⊼}_{𝑔}{v}\right)$
3 2 rexbidv ${⊢}{x}={f}\to \left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}↔\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)$
4 eqeq1 ${⊢}{x}={f}\to \left({x}=\left[{\forall }_{𝑔}{i}{u}\right]↔{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)$
5 4 rexbidv ${⊢}{x}={f}\to \left(\exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]↔\exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)$
6 3 5 orbi12d ${⊢}{x}={f}\to \left(\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)↔\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\right)$
7 6 rexbidv ${⊢}{x}={f}\to \left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)↔\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\right)$
8 2 2rexbidv ${⊢}{x}={f}\to \left(\exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}↔\exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)$
9 7 8 orbi12d ${⊢}{x}={f}\to \left(\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)↔\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)\right)$
10 1 9 elab ${⊢}{f}\in \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}↔\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)$
11 gonar ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)\to \left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \mathrm{Fmla}\left({N}\right)\right)$
12 elndif ${⊢}{u}\in \mathrm{Fmla}\left({N}\right)\to ¬{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)$
13 12 adantr ${⊢}\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)$
14 13 intnanrd ${⊢}\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
15 11 14 syl ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
16 15 ex ${⊢}{N}\in \mathrm{\omega }\to \left({u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\to ¬\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\right)$
17 16 con2d ${⊢}{N}\in \mathrm{\omega }\to \left(\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to ¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)$
18 17 impl ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to ¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)$
19 elneeldif ${⊢}\left({a}\in \mathrm{Fmla}\left({N}\right)\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to {a}\ne {u}$
20 19 necomd ${⊢}\left({a}\in \mathrm{Fmla}\left({N}\right)\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to {u}\ne {a}$
21 20 ancoms ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to {u}\ne {a}$
22 21 neneqd ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{u}={a}$
23 22 orcd ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(¬{u}={a}\vee ¬{v}={b}\right)$
24 ianor ${⊢}¬\left({u}={a}\wedge {v}={b}\right)↔\left(¬{u}={a}\vee ¬{v}={b}\right)$
25 vex ${⊢}{u}\in \mathrm{V}$
26 vex ${⊢}{v}\in \mathrm{V}$
27 25 26 opth ${⊢}⟨{u},{v}⟩=⟨{a},{b}⟩↔\left({u}={a}\wedge {v}={b}\right)$
28 24 27 xchnxbir ${⊢}¬⟨{u},{v}⟩=⟨{a},{b}⟩↔\left(¬{u}={a}\vee ¬{v}={b}\right)$
29 23 28 sylibr ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬⟨{u},{v}⟩=⟨{a},{b}⟩$
30 29 olcd ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(¬{1}_{𝑜}={1}_{𝑜}\vee ¬⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
31 ianor ${⊢}¬\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{u},{v}⟩=⟨{a},{b}⟩\right)↔\left(¬{1}_{𝑜}={1}_{𝑜}\vee ¬⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
32 gonafv ${⊢}\left({u}\in \mathrm{V}\wedge {v}\in \mathrm{V}\right)\to {u}{⊼}_{𝑔}{v}=⟨{1}_{𝑜},⟨{u},{v}⟩⟩$
33 32 el2v ${⊢}{u}{⊼}_{𝑔}{v}=⟨{1}_{𝑜},⟨{u},{v}⟩⟩$
34 gonafv ${⊢}\left({a}\in \mathrm{V}\wedge {b}\in \mathrm{V}\right)\to {a}{⊼}_{𝑔}{b}=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
35 34 el2v ${⊢}{a}{⊼}_{𝑔}{b}=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
36 33 35 eqeq12i ${⊢}{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔⟨{1}_{𝑜},⟨{u},{v}⟩⟩=⟨{1}_{𝑜},⟨{a},{b}⟩⟩$
37 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
38 opex ${⊢}⟨{u},{v}⟩\in \mathrm{V}$
39 37 38 opth ${⊢}⟨{1}_{𝑜},⟨{u},{v}⟩⟩=⟨{1}_{𝑜},⟨{a},{b}⟩⟩↔\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
40 36 39 bitri ${⊢}{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
41 31 40 xchnxbir ${⊢}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔\left(¬{1}_{𝑜}={1}_{𝑜}\vee ¬⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
42 30 41 sylibr ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
43 42 ralrimivw ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
44 43 ralrimiva ${⊢}{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
45 44 adantl ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
46 45 adantr ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
47 gonanegoal ${⊢}{u}{⊼}_{𝑔}{v}\ne \left[{\forall }_{𝑔}{j}{a}\right]$
48 47 neii ${⊢}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
49 48 a1i ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to ¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
50 49 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
51 50 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
52 r19.26 ${⊢}\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
53 46 51 52 sylanbrc ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
54 18 53 jca ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
55 eleq1 ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left({f}\in \mathrm{Fmla}\left({N}\right)↔{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)$
56 55 notbid ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)↔¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)$
57 eqeq1 ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left({f}={a}{⊼}_{𝑔}{b}↔{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\right)$
58 57 notbid ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}={a}{⊼}_{𝑔}{b}↔¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\right)$
59 58 ralbidv ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}↔\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\right)$
60 eqeq1 ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left({f}=\left[{\forall }_{𝑔}{j}{a}\right]↔{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
61 60 notbid ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]↔¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
62 61 ralbidv ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]↔\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
63 59 62 anbi12d ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
64 63 ralbidv ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
65 56 64 anbi12d ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
66 54 65 syl5ibrcom ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)\to \left({f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
67 66 rexlimdva ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
68 goalr ${⊢}\left({N}\in \mathrm{\omega }\wedge \left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\right)\to {u}\in \mathrm{Fmla}\left({N}\right)$
69 68 12 syl ${⊢}\left({N}\in \mathrm{\omega }\wedge \left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)$
70 69 ex ${⊢}{N}\in \mathrm{\omega }\to \left(\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\to ¬{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)$
71 70 con2d ${⊢}{N}\in \mathrm{\omega }\to \left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\to ¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\right)$
72 71 imp ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to ¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)$
73 72 adantr ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to ¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)$
74 gonanegoal ${⊢}{a}{⊼}_{𝑔}{b}\ne \left[{\forall }_{𝑔}{i}{u}\right]$
75 74 nesymi ${⊢}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}$
76 75 a1i ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to ¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}$
77 76 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}$
78 77 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}$
79 22 olcd ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(¬{i}={j}\vee ¬{u}={a}\right)$
80 ianor ${⊢}¬\left({i}={j}\wedge {u}={a}\right)↔\left(¬{i}={j}\vee ¬{u}={a}\right)$
81 vex ${⊢}{i}\in \mathrm{V}$
82 81 25 opth ${⊢}⟨{i},{u}⟩=⟨{j},{a}⟩↔\left({i}={j}\wedge {u}={a}\right)$
83 80 82 xchnxbir ${⊢}¬⟨{i},{u}⟩=⟨{j},{a}⟩↔\left(¬{i}={j}\vee ¬{u}={a}\right)$
84 79 83 sylibr ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬⟨{i},{u}⟩=⟨{j},{a}⟩$
85 84 olcd ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(¬{2}_{𝑜}={2}_{𝑜}\vee ¬⟨{i},{u}⟩=⟨{j},{a}⟩\right)$
86 ianor ${⊢}¬\left({2}_{𝑜}={2}_{𝑜}\wedge ⟨{i},{u}⟩=⟨{j},{a}⟩\right)↔\left(¬{2}_{𝑜}={2}_{𝑜}\vee ¬⟨{i},{u}⟩=⟨{j},{a}⟩\right)$
87 2oex ${⊢}{2}_{𝑜}\in \mathrm{V}$
88 opex ${⊢}⟨{i},{u}⟩\in \mathrm{V}$
89 87 88 opth ${⊢}⟨{2}_{𝑜},⟨{i},{u}⟩⟩=⟨{2}_{𝑜},⟨{j},{a}⟩⟩↔\left({2}_{𝑜}={2}_{𝑜}\wedge ⟨{i},{u}⟩=⟨{j},{a}⟩\right)$
90 86 89 xchnxbir ${⊢}¬⟨{2}_{𝑜},⟨{i},{u}⟩⟩=⟨{2}_{𝑜},⟨{j},{a}⟩⟩↔\left(¬{2}_{𝑜}={2}_{𝑜}\vee ¬⟨{i},{u}⟩=⟨{j},{a}⟩\right)$
91 df-goal ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]=⟨{2}_{𝑜},⟨{i},{u}⟩⟩$
92 df-goal ${⊢}\left[{\forall }_{𝑔}{j}{a}\right]=⟨{2}_{𝑜},⟨{j},{a}⟩⟩$
93 91 92 eqeq12i ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]↔⟨{2}_{𝑜},⟨{i},{u}⟩⟩=⟨{2}_{𝑜},⟨{j},{a}⟩⟩$
94 90 93 xchnxbir ${⊢}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]↔\left(¬{2}_{𝑜}={2}_{𝑜}\vee ¬⟨{i},{u}⟩=⟨{j},{a}⟩\right)$
95 85 94 sylibr ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]$
96 95 ralrimivw ${⊢}\left({u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {a}\in \mathrm{Fmla}\left({N}\right)\right)\to \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]$
97 96 ralrimiva ${⊢}{u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]$
98 97 adantl ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]$
99 98 adantr ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]$
100 r19.26 ${⊢}\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
101 78 99 100 sylanbrc ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
102 73 101 jca ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \left(¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
103 eleq1 ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)↔{f}\in \mathrm{Fmla}\left({N}\right)\right)$
104 103 notbid ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)↔¬{f}\in \mathrm{Fmla}\left({N}\right)\right)$
105 eqeq1 ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}↔{f}={a}{⊼}_{𝑔}{b}\right)$
106 105 notbid ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}↔¬{f}={a}{⊼}_{𝑔}{b}\right)$
107 106 ralbidv ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}↔\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\right)$
108 eqeq1 ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]↔{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
109 108 notbid ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]↔¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
110 109 ralbidv ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]↔\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
111 107 110 anbi12d ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
112 111 ralbidv ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
113 104 112 anbi12d ${⊢}\left[{\forall }_{𝑔}{i}{u}\right]={f}\to \left(\left(¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
114 113 eqcoms ${⊢}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\to \left(\left(¬\left[{\forall }_{𝑔}{i}{u}\right]\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left[{\forall }_{𝑔}{i}{u}\right]=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
115 102 114 syl5ibcom ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\wedge {i}\in \mathrm{\omega }\right)\to \left({f}=\left[{\forall }_{𝑔}{i}{u}\right]\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
116 115 rexlimdva ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \left(\exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
117 67 116 jaod ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \left(\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
118 117 rexlimdva ${⊢}{N}\in \mathrm{\omega }\to \left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
119 elndif ${⊢}{v}\in \mathrm{Fmla}\left({N}\right)\to ¬{v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)$
120 119 adantl ${⊢}\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)$
121 120 intnand ${⊢}\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)$
122 11 121 syl ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)$
123 122 ex ${⊢}{N}\in \mathrm{\omega }\to \left({u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\to ¬\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\right)$
124 123 con2d ${⊢}{N}\in \mathrm{\omega }\to \left(\left({u}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to ¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\right)$
125 124 impl ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to ¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)$
126 elneeldif ${⊢}\left({b}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to {b}\ne {v}$
127 126 necomd ${⊢}\left({b}\in \mathrm{Fmla}\left({N}\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to {v}\ne {b}$
128 127 ancoms ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to {v}\ne {b}$
129 128 neneqd ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{v}={b}$
130 129 olcd ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(¬{u}={a}\vee ¬{v}={b}\right)$
131 130 28 sylibr ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬⟨{u},{v}⟩=⟨{a},{b}⟩$
132 131 intnand ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬\left({1}_{𝑜}={1}_{𝑜}\wedge ⟨{u},{v}⟩=⟨{a},{b}⟩\right)$
133 132 40 sylnibr ${⊢}\left({v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\wedge {b}\in \mathrm{Fmla}\left({N}\right)\right)\to ¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
134 133 ralrimiva ${⊢}{v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\to \forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
135 134 ralrimivw ${⊢}{v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
136 135 adantl ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}$
137 48 a1i ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to ¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
138 137 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
139 138 ralrimivw ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]$
140 136 139 52 sylanbrc ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
141 125 140 jca ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
142 eleq1 ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left({u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)↔{f}\in \mathrm{Fmla}\left({N}\right)\right)$
143 142 notbid ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)↔¬{f}\in \mathrm{Fmla}\left({N}\right)\right)$
144 eqeq1 ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left({u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔{f}={a}{⊼}_{𝑔}{b}\right)$
145 144 notbid ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔¬{f}={a}{⊼}_{𝑔}{b}\right)$
146 145 ralbidv ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}↔\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\right)$
147 eqeq1 ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left({u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]↔{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
148 147 notbid ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]↔¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
149 148 ralbidv ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]↔\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
150 146 149 anbi12d ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
151 150 ralbidv ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
152 143 151 anbi12d ${⊢}{u}{⊼}_{𝑔}{v}={f}\to \left(\left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
153 152 eqcoms ${⊢}{f}={u}{⊼}_{𝑔}{v}\to \left(\left(¬{u}{⊼}_{𝑔}{v}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{u}{⊼}_{𝑔}{v}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
154 141 153 syl5ibcom ${⊢}\left(\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\wedge {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\right)\to \left({f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
155 154 rexlimdva ${⊢}\left({N}\in \mathrm{\omega }\wedge {u}\in \mathrm{Fmla}\left({N}\right)\right)\to \left(\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
156 155 rexlimdva ${⊢}{N}\in \mathrm{\omega }\to \left(\exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
157 118 156 jaod ${⊢}{N}\in \mathrm{\omega }\to \left(\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)\to \left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
158 isfmlasuc ${⊢}\left({N}\in \mathrm{\omega }\wedge {f}\in \mathrm{V}\right)\to \left({f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔\left({f}\in \mathrm{Fmla}\left({N}\right)\vee \exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
159 158 elvd ${⊢}{N}\in \mathrm{\omega }\to \left({f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔\left({f}\in \mathrm{Fmla}\left({N}\right)\vee \exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
160 159 notbid ${⊢}{N}\in \mathrm{\omega }\to \left(¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔¬\left({f}\in \mathrm{Fmla}\left({N}\right)\vee \exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
161 ioran ${⊢}¬\left({f}\in \mathrm{Fmla}\left({N}\right)\vee \exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge ¬\exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
162 ralnex ${⊢}\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}↔¬\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}$
163 ralnex ${⊢}\forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]↔¬\exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]$
164 162 163 anbi12i ${⊢}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(¬\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\wedge ¬\exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
165 ioran ${⊢}¬\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\left(¬\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\wedge ¬\exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
166 164 165 bitr4i ${⊢}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔¬\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
167 166 ralbii ${⊢}\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
168 ralnex ${⊢}\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔¬\exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
169 167 168 bitr2i ${⊢}¬\exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)↔\forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)$
170 169 anbi2i ${⊢}\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge ¬\exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
171 161 170 bitri ${⊢}¬\left({f}\in \mathrm{Fmla}\left({N}\right)\vee \exists {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\exists {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}{f}={a}{⊼}_{𝑔}{b}\vee \exists {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)$
172 160 171 syl6bb ${⊢}{N}\in \mathrm{\omega }\to \left(¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)↔\left(¬{f}\in \mathrm{Fmla}\left({N}\right)\wedge \forall {a}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {b}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}¬{f}={a}{⊼}_{𝑔}{b}\wedge \forall {j}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬{f}=\left[{\forall }_{𝑔}{j}{a}\right]\right)\right)\right)$
173 157 172 sylibrd ${⊢}{N}\in \mathrm{\omega }\to \left(\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{f}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{f}={u}{⊼}_{𝑔}{v}\right)\to ¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
174 10 173 syl5bi ${⊢}{N}\in \mathrm{\omega }\to \left({f}\in \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}\to ¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\right)$
175 174 ralrimiv ${⊢}{N}\in \mathrm{\omega }\to \forall {f}\in \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}\phantom{\rule{.4em}{0ex}}¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)$
176 disjr ${⊢}\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\cap \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}=\varnothing ↔\forall {f}\in \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}\phantom{\rule{.4em}{0ex}}¬{f}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)$
177 175 176 sylibr ${⊢}{N}\in \mathrm{\omega }\to \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\cap \left\{{x}|\left(\exists {u}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}\left(\exists {v}\in \mathrm{Fmla}\left(\mathrm{suc}{N}\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\vee \exists {i}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{x}=\left[{\forall }_{𝑔}{i}{u}\right]\right)\vee \exists {u}\in \mathrm{Fmla}\left({N}\right)\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(\mathrm{Fmla}\left(\mathrm{suc}{N}\right)\setminus \mathrm{Fmla}\left({N}\right)\right)\phantom{\rule{.4em}{0ex}}{x}={u}{⊼}_{𝑔}{v}\right)\right\}=\varnothing$