fmlasssuc

Description: The Godel formulas of height N are a subset of the Godel formulas of height N + 1 . (Contributed by AV, 20-Oct-2023)

		Ref	Expression
	Assertion	fmlasssuc	$⊢ N \in ω \to Fmla (N) \subseteq Fmla (suc N)$

Step	Hyp	Ref	Expression
1		ssun1	$⊢ Fmla (N) \subseteq Fmla (N) \cup \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
2		fmlasuc	$⊢ N \in ω \to Fmla (suc N) = Fmla (N) \cup \{x \| \exists u \in Fmla (N) (\exists v \in Fmla (N) x = u ⊼_{𝑔} v \lor \exists i \in ω x = [\forall_{𝑔} i u])\}$
3	1 2	sseqtrrid	$⊢ N \in ω \to Fmla (N) \subseteq Fmla (suc N)$

Metamath Proof Explorer