This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ N F = u ⊼ 𝑔 v ∨ ∃ i ∈ ω F = ∀ 𝑔 i u

Proof

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