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 ‘ 𝑁 ) 𝐹 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝐹 = ∀𝑔 𝑖 𝑢 ) ) ) )