Metamath Proof Explorer

Theorem satf0sucom

Description: The satisfaction predicate as function over wff codes in the empty model with an empty binary relation at a successor of _om . (Contributed by AV, 14-Sep-2023)

		Ref	Expression
	Assertion	satf0sucom	$⊢ N \in suc ω \to (\emptyset Sat \emptyset) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$

Proof

Step	Hyp	Ref	Expression
1		satf0	$⊢ \emptyset Sat \emptyset = {rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) ↾}_{suc ω}$
2	1	fveq1i	$⊢ (\emptyset Sat \emptyset) (N) = ({rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) ↾}_{suc ω}) (N)$
3		fvres	$⊢ N \in suc ω \to ({rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) ↾}_{suc ω}) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$
4	2 3	eqtrid	$⊢ N \in suc ω \to (\emptyset Sat \emptyset) (N) = rec ((f \in V ⟼ f \cup \{⟨x, y⟩ \| (y = \emptyset \land \exists u \in f (\exists v \in f x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \lor \exists i \in ω x = [\forall_{𝑔} i 1^{st} (u)]))\}), \{⟨x, y⟩ \| (y = \emptyset \land \exists i \in ω \exists j \in ω x = i \in_{𝑔} j)\}) (N)$