Metamath Proof Explorer

Theorem isfmlasuc

Description: The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023)

Ref Expression
Assertion isfmlasuc ⊢N∈ω∧F∈V→F∈Fmla⁡suc⁡N↔F∈Fmla⁡N∨∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu

Proof

Step Hyp Ref Expression
1 fmlasuc ⊢N∈ω→Fmla⁡suc⁡N=Fmla⁡N∪f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu
2 1 adantr ⊢N∈ω∧F∈V→Fmla⁡suc⁡N=Fmla⁡N∪f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu
3 2 eleq2d ⊢N∈ω∧F∈V→F∈Fmla⁡suc⁡N↔F∈Fmla⁡N∪f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu
4 elun ⊢F∈Fmla⁡N∪f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔F∈Fmla⁡N∨F∈f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu
5 4 a1i ⊢N∈ω∧F∈V→F∈Fmla⁡N∪f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔F∈Fmla⁡N∨F∈f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu
6 eqeq1 ⊢f=F→f=u⊼𝑔v↔F=u⊼𝑔v
7 6 rexbidv ⊢f=F→∃v∈Fmla⁡Nf=u⊼𝑔v↔∃v∈Fmla⁡NF=u⊼𝑔v
8 eqeq1 ⊢f=F→f=∀𝑔iu↔F=∀𝑔iu
9 8 rexbidv ⊢f=F→∃i∈ωf=∀𝑔iu↔∃i∈ωF=∀𝑔iu
10 7 9 orbi12d ⊢f=F→∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu
11 10 rexbidv ⊢f=F→∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu
12 11 elabg ⊢F∈V→F∈f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu
13 12 adantl ⊢N∈ω∧F∈V→F∈f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu
14 13 orbi2d ⊢N∈ω∧F∈V→F∈Fmla⁡N∨F∈f|∃u∈Fmla⁡N∃v∈Fmla⁡Nf=u⊼𝑔v∨∃i∈ωf=∀𝑔iu↔F∈Fmla⁡N∨∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu
15 3 5 14 3bitrd ⊢N∈ω∧F∈V→F∈Fmla⁡suc⁡N↔F∈Fmla⁡N∨∃u∈Fmla⁡N∃v∈Fmla⁡NF=u⊼𝑔v∨∃i∈ωF=∀𝑔iu