satfv0fvfmla0

Description: The value of the satisfaction predicate as function over a wff code at (/) . (Contributed by AV, 2-Nov-2023)

		Ref	Expression
	Hypothesis	satfv0fv.s	$⊢ S = M Sat E$
	Assertion	satfv0fvfmla0	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to S (\emptyset) (X) = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}$

Proof

Step	Hyp	Ref	Expression
1		satfv0fv.s	$⊢ S = M Sat E$
2		satfv0fun	$⊢ (M \in V \land E \in W) \to Fun (M Sat E) (\emptyset)$
3	1	fveq1i	$⊢ S (\emptyset) = (M Sat E) (\emptyset)$
4	3	funeqi	$⊢ Fun S (\emptyset) \leftrightarrow Fun (M Sat E) (\emptyset)$
5	2 4	sylibr	$⊢ (M \in V \land E \in W) \to Fun S (\emptyset)$
6	5	3adant3	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to Fun S (\emptyset)$
7		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
8	7	eleq2i	$⊢ X \in Fmla (\emptyset) \leftrightarrow X \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\}$
9		eqeq1	$⊢ x = X \to (x = i \in_{𝑔} j \leftrightarrow X = i \in_{𝑔} j)$
10	9	2rexbidv	$⊢ x = X \to (\exists i \in ω \exists j \in ω x = i \in_{𝑔} j \leftrightarrow \exists i \in ω \exists j \in ω X = i \in_{𝑔} j)$
11	10	elrab	$⊢ X \in \{x \in V \| \exists i \in ω \exists j \in ω x = i \in_{𝑔} j\} \leftrightarrow (X \in V \land \exists i \in ω \exists j \in ω X = i \in_{𝑔} j)$
12	8 11	bitri	$⊢ X \in Fmla (\emptyset) \leftrightarrow (X \in V \land \exists i \in ω \exists j \in ω X = i \in_{𝑔} j)$
13		simpr	$⊢ ((i \in ω \land j \in ω) \land X = i \in_{𝑔} j) \to X = i \in_{𝑔} j$
14		goel	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j = ⟨\emptyset, ⟨i, j⟩⟩$
15	14	eqeq2d	$⊢ (i \in ω \land j \in ω) \to (X = i \in_{𝑔} j \leftrightarrow X = ⟨\emptyset, ⟨i, j⟩⟩)$
16		2fveq3	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to 1^{st} (2^{nd} (X)) = 1^{st} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩))$
17		0ex	$⊢ \emptyset \in V$
18		opex	$⊢ ⟨i, j⟩ \in V$
19	17 18	op2nd	$⊢ 2^{nd} (⟨\emptyset, ⟨i, j⟩⟩) = ⟨i, j⟩$
20	19	fveq2i	$⊢ 1^{st} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩)) = 1^{st} (⟨i, j⟩)$
21		vex	$⊢ i \in V$
22		vex	$⊢ j \in V$
23	21 22	op1st	$⊢ 1^{st} (⟨i, j⟩) = i$
24	20 23	eqtri	$⊢ 1^{st} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩)) = i$
25	16 24	eqtrdi	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to 1^{st} (2^{nd} (X)) = i$
26	25	fveq2d	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to a (1^{st} (2^{nd} (X))) = a (i)$
27		2fveq3	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to 2^{nd} (2^{nd} (X)) = 2^{nd} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩))$
28	19	fveq2i	$⊢ 2^{nd} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩)) = 2^{nd} (⟨i, j⟩)$
29	21 22	op2nd	$⊢ 2^{nd} (⟨i, j⟩) = j$
30	28 29	eqtri	$⊢ 2^{nd} (2^{nd} (⟨\emptyset, ⟨i, j⟩⟩)) = j$
31	27 30	eqtrdi	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to 2^{nd} (2^{nd} (X)) = j$
32	31	fveq2d	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to a (2^{nd} (2^{nd} (X))) = a (j)$
33	26 32	breq12d	$⊢ X = ⟨\emptyset, ⟨i, j⟩⟩ \to (a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X))) \leftrightarrow a (i) E a (j))$
34	15 33	syl6bi	$⊢ (i \in ω \land j \in ω) \to (X = i \in_{𝑔} j \to (a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X))) \leftrightarrow a (i) E a (j)))$
35	34	imp	$⊢ ((i \in ω \land j \in ω) \land X = i \in_{𝑔} j) \to (a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X))) \leftrightarrow a (i) E a (j))$
36	35	rabbidv	$⊢ ((i \in ω \land j \in ω) \land X = i \in_{𝑔} j) \to \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}$
37	13 36	jca	$⊢ ((i \in ω \land j \in ω) \land X = i \in_{𝑔} j) \to (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
38	37	ex	$⊢ (i \in ω \land j \in ω) \to (X = i \in_{𝑔} j \to (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
39	38	reximdva	$⊢ i \in ω \to (\exists j \in ω X = i \in_{𝑔} j \to \exists j \in ω (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
40	39	reximia	$⊢ \exists i \in ω \exists j \in ω X = i \in_{𝑔} j \to \exists i \in ω \exists j \in ω (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
41	12 40	simplbiim	$⊢ X \in Fmla (\emptyset) \to \exists i \in ω \exists j \in ω (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
42	41	3ad2ant3	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to \exists i \in ω \exists j \in ω (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
43		simp3	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to X \in Fmla (\emptyset)$
44		ovex	$⊢ M^{ω} \in V$
45	44	rabex	$⊢ \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} \in V$
46		eqeq1	$⊢ y = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} \to (y = \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
47	9 46	bi2anan9	$⊢ (x = X \land y = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}) \to ((x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow (X = i \in_{𝑔} j \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
48	47	2rexbidv	$⊢ (x = X \land y = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}) \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 \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
49	48	opelopabga	$⊢ (X \in Fmla (\emptyset) \land \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} \in V) \to (⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in \{⟨x, y⟩ \| \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 \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
50	43 45 49	sylancl	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to (⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in \{⟨x, y⟩ \| \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 \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\} = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
51	42 50	mpbird	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to ⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
52	1	satfv0	$⊢ (M \in V \land E \in W) \to S (\emptyset) = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
53	52	eleq2d	$⊢ (M \in V \land E \in W) \to (⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in S (\emptyset) \leftrightarrow ⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\})$
54	53	3adant3	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to (⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in S (\emptyset) \leftrightarrow ⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\})$
55	51 54	mpbird	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to ⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in S (\emptyset)$
56		funopfv	$⊢ Fun S (\emptyset) \to (⟨X, \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}⟩ \in S (\emptyset) \to S (\emptyset) (X) = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\})$
57	6 55 56	sylc	$⊢ (M \in V \land E \in W \land X \in Fmla (\emptyset)) \to S (\emptyset) (X) = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (X))) E a (2^{nd} (2^{nd} (X)))\}$

Metamath Proof Explorer

Theorem satfv0fvfmla0

Proof