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