satfv0

Description: The value of the satisfaction predicate as function over wff codes at (/) . (Contributed by AV, 8-Oct-2023)

		Ref	Expression
	Hypothesis	satfv0.s	$⊢ S = M Sat E$
	Assertion	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)\})\}$

Proof

Step	Hyp	Ref	Expression
1		satfv0.s	$⊢ S = M Sat E$
2		peano1	$⊢ \emptyset \in ω$
3		elelsuc	$⊢ \emptyset \in ω \to \emptyset \in suc ω$
4	2 3	mp1i	$⊢ (M \in V \land E \in W) \to \emptyset \in suc ω$
5	1	satfvsucom	$⊢ (M \in V \land E \in W \land \emptyset \in suc ω) \to S (\emptyset) = 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)\})\}) (\emptyset)$
6	4 5	mpd3an3	$⊢ (M \in V \land E \in W) \to S (\emptyset) = 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)\})\}) (\emptyset)$
7		goelel3xp	$⊢ (i \in ω \land j \in ω) \to i \in_{𝑔} j \in (ω \times (ω \times ω))$
8		eleq1	$⊢ x = i \in_{𝑔} j \to (x \in (ω \times (ω \times ω)) \leftrightarrow i \in_{𝑔} j \in (ω \times (ω \times ω)))$
9	7 8	syl5ibrcom	$⊢ (i \in ω \land j \in ω) \to (x = i \in_{𝑔} j \to x \in (ω \times (ω \times ω)))$
10	9	adantrd	$⊢ (i \in ω \land j \in ω) \to ((x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to x \in (ω \times (ω \times ω)))$
11	10	pm4.71d	$⊢ (i \in ω \land j \in ω) \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)\}) \land x \in (ω \times (ω \times ω))))$
12	11	2rexbiia	$⊢ \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)\}) \land x \in (ω \times (ω \times ω)))$
13		r19.41vv	$⊢ \exists i \in ω \exists j \in ω ((x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land x \in (ω \times (ω \times ω))) \leftrightarrow (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land x \in (ω \times (ω \times ω)))$
14		ancom	$⊢ (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land x \in (ω \times (ω \times ω))) \leftrightarrow (x \in (ω \times (ω \times ω)) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
15	12 13 14	3bitri	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow (x \in (ω \times (ω \times ω)) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
16	15	opabbii	$⊢ \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\} = \{⟨x, y⟩ \| (x \in (ω \times (ω \times ω)) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))\}$
17		omex	$⊢ ω \in V$
18	17 17	xpex	$⊢ ω \times ω \in V$
19		xpexg	$⊢ (ω \in V \land ω \times ω \in V) \to ω \times (ω \times ω) \in V$
20		oveq1	$⊢ i = m \to i \in_{𝑔} j = m \in_{𝑔} j$
21	20	eqeq2d	$⊢ i = m \to (x = i \in_{𝑔} j \leftrightarrow x = m \in_{𝑔} j)$
22		fveq2	$⊢ i = m \to a (i) = a (m)$
23	22	breq1d	$⊢ i = m \to (a (i) E a (j) \leftrightarrow a (m) E a (j))$
24	23	rabbidv	$⊢ i = m \to \{a \in (M^{ω}) \| a (i) E a (j)\} = \{a \in (M^{ω}) \| a (m) E a (j)\}$
25	24	eqeq2d	$⊢ i = m \to (y = \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow y = \{a \in (M^{ω}) \| a (m) E a (j)\})$
26	21 25	anbi12d	$⊢ i = m \to ((x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow (x = m \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (m) E a (j)\}))$
27		oveq2	$⊢ j = n \to m \in_{𝑔} j = m \in_{𝑔} n$
28	27	eqeq2d	$⊢ j = n \to (x = m \in_{𝑔} j \leftrightarrow x = m \in_{𝑔} n)$
29		fveq2	$⊢ j = n \to a (j) = a (n)$
30	29	breq2d	$⊢ j = n \to (a (m) E a (j) \leftrightarrow a (m) E a (n))$
31	30	rabbidv	$⊢ j = n \to \{a \in (M^{ω}) \| a (m) E a (j)\} = \{a \in (M^{ω}) \| a (m) E a (n)\}$
32	31	eqeq2d	$⊢ j = n \to (y = \{a \in (M^{ω}) \| a (m) E a (j)\} \leftrightarrow y = \{a \in (M^{ω}) \| a (m) E a (n)\})$
33	28 32	anbi12d	$⊢ j = n \to ((x = m \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (m) E a (j)\}) \leftrightarrow (x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}))$
34	26 33	cbvrex2vw	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow \exists m \in ω \exists n \in ω (x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\})$
35		eqeq1	$⊢ x = i \in_{𝑔} j \to (x = m \in_{𝑔} n \leftrightarrow i \in_{𝑔} j = m \in_{𝑔} n)$
36	35	adantl	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land x = i \in_{𝑔} j) \to (x = m \in_{𝑔} n \leftrightarrow i \in_{𝑔} j = m \in_{𝑔} n)$
37		goeleq12bg	$⊢ ((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \to (i \in_{𝑔} j = m \in_{𝑔} n \leftrightarrow (i = m \land j = n))$
38	22	eqcomd	$⊢ i = m \to a (m) = a (i)$
39	29	eqcomd	$⊢ j = n \to a (n) = a (j)$
40	38 39	breqan12d	$⊢ (i = m \land j = n) \to (a (m) E a (n) \leftrightarrow a (i) E a (j))$
41	40	rabbidv	$⊢ (i = m \land j = n) \to \{a \in (M^{ω}) \| a (m) E a (n)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}$
42	37 41	syl6bi	$⊢ ((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \to (i \in_{𝑔} j = m \in_{𝑔} n \to \{a \in (M^{ω}) \| a (m) E a (n)\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
43	42	imp	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land i \in_{𝑔} j = m \in_{𝑔} n) \to \{a \in (M^{ω}) \| a (m) E a (n)\} = \{a \in (M^{ω}) \| a (i) E a (j)\}$
44		eqeq12	$⊢ (y = \{a \in (M^{ω}) \| a (m) E a (n)\} \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to (y = z \leftrightarrow \{a \in (M^{ω}) \| a (m) E a (n)\} = \{a \in (M^{ω}) \| a (i) E a (j)\})$
45	43 44	syl5ibrcom	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land i \in_{𝑔} j = m \in_{𝑔} n) \to ((y = \{a \in (M^{ω}) \| a (m) E a (n)\} \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to y = z)$
46	45	exp4b	$⊢ ((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \to (i \in_{𝑔} j = m \in_{𝑔} n \to (y = \{a \in (M^{ω}) \| a (m) E a (n)\} \to (z = \{a \in (M^{ω}) \| a (i) E a (j)\} \to y = z)))$
47	46	adantr	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land x = i \in_{𝑔} j) \to (i \in_{𝑔} j = m \in_{𝑔} n \to (y = \{a \in (M^{ω}) \| a (m) E a (n)\} \to (z = \{a \in (M^{ω}) \| a (i) E a (j)\} \to y = z)))$
48	36 47	sylbid	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land x = i \in_{𝑔} j) \to (x = m \in_{𝑔} n \to (y = \{a \in (M^{ω}) \| a (m) E a (n)\} \to (z = \{a \in (M^{ω}) \| a (i) E a (j)\} \to y = z)))$
49	48	impd	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land x = i \in_{𝑔} j) \to ((x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to (z = \{a \in (M^{ω}) \| a (i) E a (j)\} \to y = z))$
50	49	com23	$⊢ (((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \land x = i \in_{𝑔} j) \to (z = \{a \in (M^{ω}) \| a (i) E a (j)\} \to ((x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to y = z))$
51	50	expimpd	$⊢ ((m \in ω \land n \in ω) \land (i \in ω \land j \in ω)) \to ((x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to y = z))$
52	51	rexlimdvva	$⊢ (m \in ω \land n \in ω) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to ((x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to y = z))$
53	52	com23	$⊢ (m \in ω \land n \in ω) \to ((x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to y = z))$
54	53	rexlimivv	$⊢ \exists m \in ω \exists n \in ω (x = m \in_{𝑔} n \land y = \{a \in (M^{ω}) \| a (m) E a (n)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to y = z)$
55	34 54	sylbi	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to y = z)$
56	55	imp	$⊢ (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to y = z$
57	56	gen2	$⊢ \forall y \forall z ((\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to y = z)$
58		eqeq1	$⊢ y = z \to (y = \{a \in (M^{ω}) \| a (i) E a (j)\} \leftrightarrow z = \{a \in (M^{ω}) \| a (i) E a (j)\})$
59	58	anbi2d	$⊢ y = z \to ((x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
60	59	2rexbidv	$⊢ y = z \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 z = \{a \in (M^{ω}) \| a (i) E a (j)\}))$
61	60	mo4	$⊢ \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \leftrightarrow \forall y \forall z ((\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{a \in (M^{ω}) \| a (i) E a (j)\})) \to y = z)$
62	57 61	mpbir	$⊢ \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})$
63		moabex	$⊢ \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}) \to \{y \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\} \in V$
64	62 63	mp1i	$⊢ ((ω \in V \land ω \times ω \in V) \land x \in (ω \times (ω \times ω))) \to \{y \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\} \in V$
65	19 64	opabex3d	$⊢ (ω \in V \land ω \times ω \in V) \to \{⟨x, y⟩ \| (x \in (ω \times (ω \times ω)) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))\} \in V$
66	17 18 65	mp2an	$⊢ \{⟨x, y⟩ \| (x \in (ω \times (ω \times ω)) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\}))\} \in V$
67	16 66	eqeltri	$⊢ \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\} \in V$
68	67	rdg0	$⊢ 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)\})\}) (\emptyset) = \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{a \in (M^{ω}) \| a (i) E a (j)\})\}$
69	6 68	eqtrdi	$⊢ (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)\})\}$

Metamath Proof Explorer

Theorem satfv0

Proof