satfrel

Description: The value of the satisfaction predicate as function over wff codes at a natural number is a relation. (Contributed by AV, 12-Oct-2023)

		Ref	Expression
	Assertion	satfrel	$⊢ (M \in V \land E \in W \land N \in ω) \to Rel (M Sat E) (N)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ a = \emptyset \to (M Sat E) (a) = (M Sat E) (\emptyset)$
2	1	releqd	$⊢ a = \emptyset \to (Rel (M Sat E) (a) \leftrightarrow Rel (M Sat E) (\emptyset))$
3	2	imbi2d	$⊢ a = \emptyset \to (((M \in V \land E \in W) \to Rel (M Sat E) (a)) \leftrightarrow ((M \in V \land E \in W) \to Rel (M Sat E) (\emptyset)))$
4		fveq2	$⊢ a = b \to (M Sat E) (a) = (M Sat E) (b)$
5	4	releqd	$⊢ a = b \to (Rel (M Sat E) (a) \leftrightarrow Rel (M Sat E) (b))$
6	5	imbi2d	$⊢ a = b \to (((M \in V \land E \in W) \to Rel (M Sat E) (a)) \leftrightarrow ((M \in V \land E \in W) \to Rel (M Sat E) (b)))$
7		fveq2	$⊢ a = suc b \to (M Sat E) (a) = (M Sat E) (suc b)$
8	7	releqd	$⊢ a = suc b \to (Rel (M Sat E) (a) \leftrightarrow Rel (M Sat E) (suc b))$
9	8	imbi2d	$⊢ a = suc b \to (((M \in V \land E \in W) \to Rel (M Sat E) (a)) \leftrightarrow ((M \in V \land E \in W) \to Rel (M Sat E) (suc b)))$
10		fveq2	$⊢ a = N \to (M Sat E) (a) = (M Sat E) (N)$
11	10	releqd	$⊢ a = N \to (Rel (M Sat E) (a) \leftrightarrow Rel (M Sat E) (N))$
12	11	imbi2d	$⊢ a = N \to (((M \in V \land E \in W) \to Rel (M Sat E) (a)) \leftrightarrow ((M \in V \land E \in W) \to Rel (M Sat E) (N)))$
13		relopab	$⊢ Rel \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
14		eqid	$⊢ M Sat E = M Sat E$
15	14	satfv0	$⊢ (M \in V \land E \in W) \to (M Sat E) (\emptyset) = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
16	15	releqd	$⊢ (M \in V \land E \in W) \to (Rel (M Sat E) (\emptyset) \leftrightarrow Rel \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\})$
17	13 16	mpbiri	$⊢ (M \in V \land E \in W) \to Rel (M Sat E) (\emptyset)$
18		pm2.27	$⊢ (M \in V \land E \in W) \to (((M \in V \land E \in W) \to Rel (M Sat E) (b)) \to Rel (M Sat E) (b))$
19		simpr	$⊢ (((M \in V \land E \in W) \land b \in ω) \land Rel (M Sat E) (b)) \to Rel (M Sat E) (b)$
20		relopab	$⊢ Rel \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\}$
21		relun	$⊢ Rel ((M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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 (Rel (M Sat E) (b) \land Rel \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\})$
22	19 20 21	sylanblrc	$⊢ (((M \in V \land E \in W) \land b \in ω) \land Rel (M Sat E) (b)) \to Rel ((M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\})$
23	14	satfvsuc	$⊢ (M \in V \land E \in W \land b \in ω) \to (M Sat E) (suc b) = (M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\}$
24	23	ad4ant123	$⊢ (((M \in V \land E \in W) \land b \in ω) \land Rel (M Sat E) (b)) \to (M Sat E) (suc b) = (M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\}$
25	24	releqd	$⊢ (((M \in V \land E \in W) \land b \in ω) \land Rel (M Sat E) (b)) \to (Rel (M Sat E) (suc b) \leftrightarrow Rel ((M Sat E) (b) \cup \{⟨x, y⟩ \| \exists u \in (M Sat E) (b) (\exists v \in (M Sat E) (b) (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)\}))\}))$
26	22 25	mpbird	$⊢ (((M \in V \land E \in W) \land b \in ω) \land Rel (M Sat E) (b)) \to Rel (M Sat E) (suc b)$
27	26	exp31	$⊢ (M \in V \land E \in W) \to (b \in ω \to (Rel (M Sat E) (b) \to Rel (M Sat E) (suc b)))$
28	27	com23	$⊢ (M \in V \land E \in W) \to (Rel (M Sat E) (b) \to (b \in ω \to Rel (M Sat E) (suc b)))$
29	18 28	syld	$⊢ (M \in V \land E \in W) \to (((M \in V \land E \in W) \to Rel (M Sat E) (b)) \to (b \in ω \to Rel (M Sat E) (suc b)))$
30	29	com13	$⊢ b \in ω \to (((M \in V \land E \in W) \to Rel (M Sat E) (b)) \to ((M \in V \land E \in W) \to Rel (M Sat E) (suc b)))$
31	3 6 9 12 17 30	finds	$⊢ N \in ω \to ((M \in V \land E \in W) \to Rel (M Sat E) (N))$
32	31	com12	$⊢ (M \in V \land E \in W) \to (N \in ω \to Rel (M Sat E) (N))$
33	32	3impia	$⊢ (M \in V \land E \in W \land N \in ω) \to Rel (M Sat E) (N)$

Metamath Proof Explorer

Theorem satfrel

Proof