Metamath Proof Explorer

Theorem satom

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

		Ref	Expression
	Assertion	satom	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) = ⋃_{n \in ω} (M Sat E) (n)$

Proof

Step	Hyp	Ref	Expression
1		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 ω}$
2	1	fveq1d	$⊢ (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 ω}) (ω)$
3		omex	$⊢ ω \in V$
4	3	sucid	$⊢ ω \in suc ω$
5		fvres	$⊢ ω \in suc ω \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 ω}) (ω) = 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)\})\}) (ω)$
6	4 5	mp1i	$⊢ (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 ω}) (ω) = 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)\})\}) (ω)$
7		limom	$⊢ Lim ω$
8	3 7	pm3.2i	$⊢ (ω \in V \land Lim ω)$
9		rdglim2a	$⊢ (ω \in V \land Lim ω) \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)\})\}) (ω) = ⋃_{n \in ω} 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)\})\}) (n)$
10	8 9	mp1i	$⊢ (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)\})\}) (ω) = ⋃_{n \in ω} 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)\})\}) (n)$
11	1	fveq1d	$⊢ (M \in V \land E \in W) \to (M Sat E) (n) = ({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 ω}) (n)$
12	11	adantr	$⊢ ((M \in V \land E \in W) \land n \in ω) \to (M Sat E) (n) = ({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 ω}) (n)$
13		elelsuc	$⊢ n \in ω \to n \in suc ω$
14	13	adantl	$⊢ ((M \in V \land E \in W) \land n \in ω) \to n \in suc ω$
15	14	fvresd	$⊢ ((M \in V \land E \in W) \land n \in ω) \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 ω}) (n) = 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)\})\}) (n)$
16	12 15	eqtr2d	$⊢ ((M \in V \land E \in W) \land n \in ω) \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)\})\}) (n) = (M Sat E) (n)$
17	16	iuneq2dv	$⊢ (M \in V \land E \in W) \to ⋃_{n \in ω} 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)\})\}) (n) = ⋃_{n \in ω} (M Sat E) (n)$
18	10 17	eqtrd	$⊢ (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)\})\}) (ω) = ⋃_{n \in ω} (M Sat E) (n)$
19	2 6 18	3eqtrd	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) = ⋃_{n \in ω} (M Sat E) (n)$