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 ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) )

Proof

Step Hyp Ref Expression
1 fmlasuc ⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) )
2 1 adantr ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) )
3 2 eleq2d ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑁 ) ↔ 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) )
4 elun ⊢ ( 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) )
5 4 a1i ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ) )
6 eqeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
7 6 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
8 eqeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ∀𝑔 𝑖 𝑢 ↔ 𝐹 = ∀𝑔 𝑖 𝑢 ) )
9 8 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) )
10 7 9 orbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) )
11 10 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) )
12 11 elabg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) )
13 12 adantl ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) )
14 13 orbi2d ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ 𝐹 ∈ { 𝑓 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑓 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑓 = ∀𝑔 𝑖 𝑢 ) } ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) )
15 3 5 14 3bitrd ⊢ ( ( 𝑁 ∈ ω ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ ( Fmla ‘ suc 𝑁 ) ↔ ( 𝐹 ∈ ( Fmla ‘ 𝑁 ) ∨ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝐹 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) )