Metamath Proof Explorer

Theorem satfn

Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M is a function over suc _om . (Contributed by AV, 6-Oct-2023)

		Ref	Expression
	Assertion	satfn	$⊢ (M \in V \land E \in W) \to (M Sat E) Fn suc ω$

Proof

Step	Hyp	Ref	Expression
1		rdgfnon	$⊢ rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) Fn On$
2	1	a1i	$⊢ (M \in V \land E \in W) \to rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) Fn On$
3		ordom	$⊢ Ord ω$
4		ordsuc	$⊢ Ord ω \leftrightarrow Ord suc ω$
5	3 4	mpbi	$⊢ Ord suc ω$
6		ordsson	$⊢ Ord suc ω \to suc ω \subseteq On$
7	5 6	mp1i	$⊢ (M \in V \land E \in W) \to suc ω \subseteq On$
8	2 7	fnssresd	$⊢ (M \in V \land E \in W) \to ({rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) ↾}_{suc ω}) Fn suc ω$
9		satf	$⊢ (M \in V \land E \in W) \to M Sat E = {rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) ↾}_{suc ω}$
10	9	fneq1d	$⊢ (M \in V \land E \in W) \to ((M Sat E) Fn suc ω \leftrightarrow ({rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| \exists u \in f (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \lor \exists i \in ω (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))\}), \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) ↾}_{suc ω}) Fn suc ω)$
11	8 10	mpbird	$⊢ (M \in V \land E \in W) \to (M Sat E) Fn suc ω$