sategoelfvb

Description: Characterization of a valuation S of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023)

		Ref	Expression
	Hypothesis	sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
	Assertion	sategoelfvb	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
2		ovexd	$⊢ (A \in ω \land B \in ω) \to A \in_{𝑔} B \in V$
3		simpl	$⊢ (A \in ω \land B \in ω) \to A \in ω$
4		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
5	4	opeq2d	$⊢ a = A \to ⟨\emptyset, ⟨a, b⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩$
6	5	eqeq2d	$⊢ a = A \to (⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩ \leftrightarrow ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩)$
7	6	rexbidv	$⊢ a = A \to (\exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩ \leftrightarrow \exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩)$
8	7	adantl	$⊢ ((A \in ω \land B \in ω) \land a = A) \to (\exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩ \leftrightarrow \exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩)$
9		simpr	$⊢ (A \in ω \land B \in ω) \to B \in ω$
10		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
11	10	opeq2d	$⊢ b = B \to ⟨\emptyset, ⟨A, b⟩⟩ = ⟨\emptyset, ⟨A, B⟩⟩$
12	11	eqeq2d	$⊢ b = B \to (⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩ \leftrightarrow ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, B⟩⟩)$
13	12	adantl	$⊢ ((A \in ω \land B \in ω) \land b = B) \to (⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩ \leftrightarrow ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, B⟩⟩)$
14		eqidd	$⊢ (A \in ω \land B \in ω) \to ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, B⟩⟩$
15	9 13 14	rspcedvd	$⊢ (A \in ω \land B \in ω) \to \exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨A, b⟩⟩$
16	3 8 15	rspcedvd	$⊢ (A \in ω \land B \in ω) \to \exists a \in ω \exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩$
17		goel	$⊢ (A \in ω \land B \in ω) \to A \in_{𝑔} B = ⟨\emptyset, ⟨A, B⟩⟩$
18		goel	$⊢ (a \in ω \land b \in ω) \to a \in_{𝑔} b = ⟨\emptyset, ⟨a, b⟩⟩$
19	17 18	eqeqan12d	$⊢ ((A \in ω \land B \in ω) \land (a \in ω \land b \in ω)) \to (A \in_{𝑔} B = a \in_{𝑔} b \leftrightarrow ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩)$
20	19	2rexbidva	$⊢ (A \in ω \land B \in ω) \to (\exists a \in ω \exists b \in ω A \in_{𝑔} B = a \in_{𝑔} b \leftrightarrow \exists a \in ω \exists b \in ω ⟨\emptyset, ⟨A, B⟩⟩ = ⟨\emptyset, ⟨a, b⟩⟩)$
21	16 20	mpbird	$⊢ (A \in ω \land B \in ω) \to \exists a \in ω \exists b \in ω A \in_{𝑔} B = a \in_{𝑔} b$
22		eqeq1	$⊢ x = A \in_{𝑔} B \to (x = a \in_{𝑔} b \leftrightarrow A \in_{𝑔} B = a \in_{𝑔} b)$
23	22	2rexbidv	$⊢ x = A \in_{𝑔} B \to (\exists a \in ω \exists b \in ω x = a \in_{𝑔} b \leftrightarrow \exists a \in ω \exists b \in ω A \in_{𝑔} B = a \in_{𝑔} b)$
24		fmla0	$⊢ Fmla (\emptyset) = \{x \in V \| \exists a \in ω \exists b \in ω x = a \in_{𝑔} b\}$
25	23 24	elrab2	$⊢ A \in_{𝑔} B \in Fmla (\emptyset) \leftrightarrow (A \in_{𝑔} B \in V \land \exists a \in ω \exists b \in ω A \in_{𝑔} B = a \in_{𝑔} b)$
26	2 21 25	sylanbrc	$⊢ (A \in ω \land B \in ω) \to A \in_{𝑔} B \in Fmla (\emptyset)$
27		satefvfmla0	$⊢ (M \in V \land A \in_{𝑔} B \in Fmla (\emptyset)) \to M {Sat}_{\in} (A \in_{𝑔} B) = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B)))\}$
28	26 27	sylan2	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to M {Sat}_{\in} (A \in_{𝑔} B) = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B)))\}$
29	1 28	syl5eq	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to E = \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B)))\}$
30	29	eleq2d	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow S \in \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B)))\})$
31		fveq1	$⊢ a = S \to a (1^{st} (2^{nd} (A \in_{𝑔} B))) = S (1^{st} (2^{nd} (A \in_{𝑔} B)))$
32		fveq1	$⊢ a = S \to a (2^{nd} (2^{nd} (A \in_{𝑔} B))) = S (2^{nd} (2^{nd} (A \in_{𝑔} B)))$
33	31 32	eleq12d	$⊢ a = S \to (a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B))) \leftrightarrow S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B))))$
34	33	elrab	$⊢ S \in \{a \in (M^{ω}) \| a (1^{st} (2^{nd} (A \in_{𝑔} B))) \in a (2^{nd} (2^{nd} (A \in_{𝑔} B)))\} \leftrightarrow (S \in (M^{ω}) \land S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B))))$
35	30 34	bitrdi	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B)))))$
36	17	fveq2d	$⊢ (A \in ω \land B \in ω) \to 2^{nd} (A \in_{𝑔} B) = 2^{nd} (⟨\emptyset, ⟨A, B⟩⟩)$
37	36	fveq2d	$⊢ (A \in ω \land B \in ω) \to 1^{st} (2^{nd} (A \in_{𝑔} B)) = 1^{st} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩))$
38		0ex	$⊢ \emptyset \in V$
39		opex	$⊢ ⟨A, B⟩ \in V$
40	38 39	op2nd	$⊢ 2^{nd} (⟨\emptyset, ⟨A, B⟩⟩) = ⟨A, B⟩$
41	40	fveq2i	$⊢ 1^{st} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩)) = 1^{st} (⟨A, B⟩)$
42		op1stg	$⊢ (A \in ω \land B \in ω) \to 1^{st} (⟨A, B⟩) = A$
43	41 42	syl5eq	$⊢ (A \in ω \land B \in ω) \to 1^{st} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩)) = A$
44	37 43	eqtrd	$⊢ (A \in ω \land B \in ω) \to 1^{st} (2^{nd} (A \in_{𝑔} B)) = A$
45	44	fveq2d	$⊢ (A \in ω \land B \in ω) \to S (1^{st} (2^{nd} (A \in_{𝑔} B))) = S (A)$
46	36	fveq2d	$⊢ (A \in ω \land B \in ω) \to 2^{nd} (2^{nd} (A \in_{𝑔} B)) = 2^{nd} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩))$
47	40	fveq2i	$⊢ 2^{nd} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩)) = 2^{nd} (⟨A, B⟩)$
48		op2ndg	$⊢ (A \in ω \land B \in ω) \to 2^{nd} (⟨A, B⟩) = B$
49	47 48	syl5eq	$⊢ (A \in ω \land B \in ω) \to 2^{nd} (2^{nd} (⟨\emptyset, ⟨A, B⟩⟩)) = B$
50	46 49	eqtrd	$⊢ (A \in ω \land B \in ω) \to 2^{nd} (2^{nd} (A \in_{𝑔} B)) = B$
51	50	fveq2d	$⊢ (A \in ω \land B \in ω) \to S (2^{nd} (2^{nd} (A \in_{𝑔} B))) = S (B)$
52	45 51	eleq12d	$⊢ (A \in ω \land B \in ω) \to (S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B))) \leftrightarrow S (A) \in S (B))$
53	52	adantl	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B))) \leftrightarrow S (A) \in S (B))$
54	53	anbi2d	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to ((S \in (M^{ω}) \land S (1^{st} (2^{nd} (A \in_{𝑔} B))) \in S (2^{nd} (2^{nd} (A \in_{𝑔} B)))) \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$
55	35 54	bitrd	$⊢ (M \in V \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$

Metamath Proof Explorer

Theorem sategoelfvb

Proof