ex-sategoelel

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

	Ref	Expression
Hypotheses	sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
	ex-sategoelel.s	$⊢ S = (x \in ω ⟼ if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)))$
Assertion	ex-sategoelel	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S \in E$

Proof

Step	Hyp	Ref	Expression
1		sategoelfvb.s	$⊢ E = M {Sat}_{\in} (A \in_{𝑔} B)$
2		ex-sategoelel.s	$⊢ S = (x \in ω ⟼ if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)))$
3		simpr	$⊢ (M \in WUni \land Z \in M) \to Z \in M$
4		simpl	$⊢ (M \in WUni \land Z \in M) \to M \in WUni$
5	4 3	wunpw	$⊢ (M \in WUni \land Z \in M) \to 𝒫 Z \in M$
6	4	wun0	$⊢ (M \in WUni \land Z \in M) \to \emptyset \in M$
7	5 6	ifcld	$⊢ (M \in WUni \land Z \in M) \to if (x = B, 𝒫 Z, \emptyset) \in M$
8	3 7	ifcld	$⊢ (M \in WUni \land Z \in M) \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) \in M$
9	8	adantr	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) \in M$
10	9	adantr	$⊢ (((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \land x \in ω) \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) \in M$
11	10 2	fmptd	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S : ω ⟶ M$
12	4	adantr	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to M \in WUni$
13		omex	$⊢ ω \in V$
14	13	a1i	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to ω \in V$
15	12 14	elmapd	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to (S \in (M^{ω}) \leftrightarrow S : ω ⟶ M)$
16	11 15	mpbird	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S \in (M^{ω})$
17		pwidg	$⊢ Z \in M \to Z \in 𝒫 Z$
18	17	adantl	$⊢ (M \in WUni \land Z \in M) \to Z \in 𝒫 Z$
19	18	adantr	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to Z \in 𝒫 Z$
20	2	a1i	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S = (x \in ω ⟼ if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)))$
21		iftrue	$⊢ x = A \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) = Z$
22	21	adantl	$⊢ (((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \land x = A) \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) = Z$
23		simpr1	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to A \in ω$
24	3	adantr	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to Z \in M$
25	20 22 23 24	fvmptd	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (A) = Z$
26		eqeq1	$⊢ x = B \to (x = A \leftrightarrow B = A)$
27		eqeq1	$⊢ x = B \to (x = B \leftrightarrow B = B)$
28	27	ifbid	$⊢ x = B \to if (x = B, 𝒫 Z, \emptyset) = if (B = B, 𝒫 Z, \emptyset)$
29	26 28	ifbieq2d	$⊢ x = B \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) = if (B = A, Z, if (B = B, 𝒫 Z, \emptyset))$
30		necom	$⊢ A \neq B \leftrightarrow B \neq A$
31		ifnefalse	$⊢ B \neq A \to if (B = A, Z, if (B = B, 𝒫 Z, \emptyset)) = if (B = B, 𝒫 Z, \emptyset)$
32	30 31	sylbi	$⊢ A \neq B \to if (B = A, Z, if (B = B, 𝒫 Z, \emptyset)) = if (B = B, 𝒫 Z, \emptyset)$
33	32	3ad2ant3	$⊢ (A \in ω \land B \in ω \land A \neq B) \to if (B = A, Z, if (B = B, 𝒫 Z, \emptyset)) = if (B = B, 𝒫 Z, \emptyset)$
34	33	adantl	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to if (B = A, Z, if (B = B, 𝒫 Z, \emptyset)) = if (B = B, 𝒫 Z, \emptyset)$
35	29 34	sylan9eqr	$⊢ (((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \land x = B) \to if (x = A, Z, if (x = B, 𝒫 Z, \emptyset)) = if (B = B, 𝒫 Z, \emptyset)$
36		simpr2	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to B \in ω$
37		pwexg	$⊢ Z \in M \to 𝒫 Z \in V$
38	37	adantl	$⊢ (M \in WUni \land Z \in M) \to 𝒫 Z \in V$
39		0ex	$⊢ \emptyset \in V$
40	39	a1i	$⊢ (M \in WUni \land Z \in M) \to \emptyset \in V$
41	38 40	ifcld	$⊢ (M \in WUni \land Z \in M) \to if (B = B, 𝒫 Z, \emptyset) \in V$
42	41	adantr	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to if (B = B, 𝒫 Z, \emptyset) \in V$
43	20 35 36 42	fvmptd	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (B) = if (B = B, 𝒫 Z, \emptyset)$
44		eqid	$⊢ B = B$
45	44	iftruei	$⊢ if (B = B, 𝒫 Z, \emptyset) = 𝒫 Z$
46	43 45	eqtrdi	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (B) = 𝒫 Z$
47	19 25 46	3eltr4d	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S (A) \in S (B)$
48		3simpa	$⊢ (A \in ω \land B \in ω \land A \neq B) \to (A \in ω \land B \in ω)$
49	1	sategoelfvb	$⊢ (M \in WUni \land (A \in ω \land B \in ω)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$
50	4 48 49	syl2an	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to (S \in E \leftrightarrow (S \in (M^{ω}) \land S (A) \in S (B)))$
51	16 47 50	mpbir2and	$⊢ ((M \in WUni \land Z \in M) \land (A \in ω \land B \in ω \land A \neq B)) \to S \in E$

Metamath Proof Explorer

Theorem ex-sategoelel

Proof