satf

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 14-Sep-2023)

		Ref	Expression
	Assertion	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 ω}$

Proof

Step	Hyp	Ref	Expression
1		df-sat	$⊢ Sat = (m \in V, e \in V ⟼ {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	a1i	$⊢ (M \in V \land E \in W) \to Sat = (m \in V, e \in V ⟼ {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		oveq1	$⊢ m = M \to m^{ω} = M^{ω}$
4	3	adantr	$⊢ (m = M \land e = E) \to m^{ω} = M^{ω}$
5	4	difeq1d	$⊢ (m = M \land e = E) \to (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))$
6	5	eqeq2d	$⊢ (m = M \land e = E) \to (y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)) \leftrightarrow y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v)))$
7	6	anbi2d	$⊢ (m = M \land e = E) \to ((x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
8	7	rexbidv	$⊢ (m = M \land e = E) \to (\exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (m^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))) \leftrightarrow \exists v \in f (x = 1^{st} (u) ⊼_{𝑔} 1^{st} (v) \land y = (M^{ω}) ∖ (2^{nd} (u) \cap 2^{nd} (v))))$
9		simpl	$⊢ (m = M \land e = E) \to m = M$
10	9	raleqdv	$⊢ (m = M \land e = E) \to (\forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u) \leftrightarrow \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u))$
11	4 10	rabeqbidv	$⊢ (m = M \land e = E) \to \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}$
12	11	eqeq2d	$⊢ (m = M \land e = E) \to (y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\} \leftrightarrow y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\})$
13	12	anbi2d	$⊢ (m = M \land e = E) \to ((x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (m^{ω}) \| \forall z \in m \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}) \leftrightarrow (x = [\forall_{𝑔} i 1^{st} (u)] \land y = \{a \in (M^{ω}) \| \forall z \in M \{⟨i, z⟩\} \cup ({a ↾}_{(ω ∖ \{i\})}) \in 2^{nd} (u)\}))$
14	13	rexbidv	$⊢ (m = M \land e = E) \to (\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)\}) \leftrightarrow \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)\}))$
15	8 14	orbi12d	$⊢ (m = M \land e = E) \to ((\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)\})) \leftrightarrow (\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)\})))$
16	15	rexbidv	$⊢ (m = M \land e = E) \to (\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)\})) \leftrightarrow \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)\})))$
17	16	opabbidv	$⊢ (m = M \land e = E) \to \{⟨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 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)\}))\}$
18	17	uneq2d	$⊢ (m = M \land e = E) \to 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)\}))\} = 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)\}))\}$
19	18	mpteq2dv	$⊢ (m = M \land e = E) \to (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)\}))\}) = (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)\}))\})$
20		breq	$⊢ e = E \to (a (i) e a (j) \leftrightarrow a (i) E a (j))$
21	20	adantl	$⊢ (m = M \land e = E) \to (a (i) e a (j) \leftrightarrow a (i) E a (j))$
22	4 21	rabeqbidv	$⊢ (m = M \land e = E) \to \{a \in (m^{ω}) \| a (i) e a (j)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}$
23	22	eqeq2d	$⊢ (m = M \land e = E) \to (y = \{a \in (m^{ω}) \| a (i) e a (j)\} \leftrightarrow y = \{a \in (M^{ω}) \| a (i) E a (j)\})$
24	23	anbi2d	$⊢ (m = M \land e = E) \to ((x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\}) \leftrightarrow (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
25	24	2rexbidv	$⊢ (m = M \land e = E) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\}) \leftrightarrow \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
26	25	opabbidv	$⊢ (m = M \land e = E) \to \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\} = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
27		rdgeq12	$⊢ ((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)\}))\}) = (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)\}))\}) \land \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (m^{ω}) \| a (i) e a (j)\})\} = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}) \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)\})\}) = 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)\})\})$
28	19 26 27	syl2anc	$⊢ (m = M \land e = E) \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)\})\}) = 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)\})\})$
29	28	reseq1d	$⊢ (m = M \land e = E) \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)\})\}) ↾}_{suc ω}$
30	29	adantl	$⊢ ((M \in V \land E \in W) \land (m = M \land e = E)) \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)\})\}) ↾}_{suc ω}$
31		elex	$⊢ M \in V \to M \in V$
32	31	adantr	$⊢ (M \in V \land E \in W) \to M \in V$
33		elex	$⊢ E \in W \to E \in V$
34	33	adantl	$⊢ (M \in V \land E \in W) \to E \in V$
35		rdgfun	$⊢ Fun 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)\})\})$
36		omex	$⊢ ω \in V$
37	36	sucex	$⊢ suc ω \in V$
38	37	a1i	$⊢ (M \in V \land E \in W) \to suc ω \in V$
39		resfunexg	$⊢ (Fun 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)\})\}) \land suc ω \in V) \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 ω} \in V$
40	35 38 39	sylancr	$⊢ (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 ω} \in V$
41	2 30 32 34 40	ovmpod	$⊢ (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 ω}$

Metamath Proof Explorer

Theorem satf

Proof