satfv0fun

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

		Ref	Expression
	Assertion	satfv0fun	$⊢ (M \in V \land E \in W) \to Fun (M Sat E) (\emptyset)$

Proof

Step	Hyp	Ref	Expression
1		funopab	$⊢ Fun \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\} \leftrightarrow \forall x \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})$
2		oveq1	$⊢ i = k \to i \in_{𝑔} j = k \in_{𝑔} j$
3	2	eqeq2d	$⊢ i = k \to (x = i \in_{𝑔} j \leftrightarrow x = k \in_{𝑔} j)$
4		fveq2	$⊢ i = k \to f (i) = f (k)$
5	4	breq1d	$⊢ i = k \to (f (i) E f (j) \leftrightarrow f (k) E f (j))$
6	5	rabbidv	$⊢ i = k \to \{f \in (M^{ω}) \| f (i) E f (j)\} = \{f \in (M^{ω}) \| f (k) E f (j)\}$
7	6	eqeq2d	$⊢ i = k \to (y = \{f \in (M^{ω}) \| f (i) E f (j)\} \leftrightarrow y = \{f \in (M^{ω}) \| f (k) E f (j)\})$
8	3 7	anbi12d	$⊢ i = k \to ((x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow (x = k \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (k) E f (j)\}))$
9		oveq2	$⊢ j = l \to k \in_{𝑔} j = k \in_{𝑔} l$
10	9	eqeq2d	$⊢ j = l \to (x = k \in_{𝑔} j \leftrightarrow x = k \in_{𝑔} l)$
11		fveq2	$⊢ j = l \to f (j) = f (l)$
12	11	breq2d	$⊢ j = l \to (f (k) E f (j) \leftrightarrow f (k) E f (l))$
13	12	rabbidv	$⊢ j = l \to \{f \in (M^{ω}) \| f (k) E f (j)\} = \{f \in (M^{ω}) \| f (k) E f (l)\}$
14	13	eqeq2d	$⊢ j = l \to (y = \{f \in (M^{ω}) \| f (k) E f (j)\} \leftrightarrow y = \{f \in (M^{ω}) \| f (k) E f (l)\})$
15	10 14	anbi12d	$⊢ j = l \to ((x = k \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (k) E f (j)\}) \leftrightarrow (x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}))$
16	8 15	cbvrex2vw	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow \exists k \in ω \exists l \in ω (x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\})$
17		eqtr2	$⊢ (x = i \in_{𝑔} j \land x = k \in_{𝑔} l) \to i \in_{𝑔} j = k \in_{𝑔} l$
18		goeleq12bg	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to (i \in_{𝑔} j = k \in_{𝑔} l \leftrightarrow (i = k \land j = l))$
19	4	adantr	$⊢ (i = k \land j = l) \to f (i) = f (k)$
20	19	eqcomd	$⊢ (i = k \land j = l) \to f (k) = f (i)$
21	11	adantl	$⊢ (i = k \land j = l) \to f (j) = f (l)$
22	21	eqcomd	$⊢ (i = k \land j = l) \to f (l) = f (j)$
23	20 22	breq12d	$⊢ (i = k \land j = l) \to (f (k) E f (l) \leftrightarrow f (i) E f (j))$
24	23	rabbidv	$⊢ (i = k \land j = l) \to \{f \in (M^{ω}) \| f (k) E f (l)\} = \{f \in (M^{ω}) \| f (i) E f (j)\}$
25		eqeq12	$⊢ (y = \{f \in (M^{ω}) \| f (k) E f (l)\} \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to (y = z \leftrightarrow \{f \in (M^{ω}) \| f (k) E f (l)\} = \{f \in (M^{ω}) \| f (i) E f (j)\})$
26	24 25	syl5ibrcom	$⊢ (i = k \land j = l) \to ((y = \{f \in (M^{ω}) \| f (k) E f (l)\} \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to y = z)$
27	26	expd	$⊢ (i = k \land j = l) \to (y = \{f \in (M^{ω}) \| f (k) E f (l)\} \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to y = z))$
28	18 27	syl6bi	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to (i \in_{𝑔} j = k \in_{𝑔} l \to (y = \{f \in (M^{ω}) \| f (k) E f (l)\} \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to y = z)))$
29	17 28	syl5	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to ((x = i \in_{𝑔} j \land x = k \in_{𝑔} l) \to (y = \{f \in (M^{ω}) \| f (k) E f (l)\} \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to y = z)))$
30	29	expd	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to (x = i \in_{𝑔} j \to (x = k \in_{𝑔} l \to (y = \{f \in (M^{ω}) \| f (k) E f (l)\} \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to y = z))))$
31	30	imp4a	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to (x = i \in_{𝑔} j \to ((x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to y = z)))$
32	31	com34	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to (x = i \in_{𝑔} j \to (z = \{f \in (M^{ω}) \| f (i) E f (j)\} \to ((x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to y = z)))$
33	32	impd	$⊢ ((k \in ω \land l \in ω) \land (i \in ω \land j \in ω)) \to ((x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to ((x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to y = z))$
34	33	rexlimdvva	$⊢ (k \in ω \land l \in ω) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to ((x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to y = z))$
35	34	com23	$⊢ (k \in ω \land l \in ω) \to ((x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to y = z))$
36	35	rexlimivv	$⊢ \exists k \in ω \exists l \in ω (x = k \in_{𝑔} l \land y = \{f \in (M^{ω}) \| f (k) E f (l)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to y = z)$
37	16 36	sylbi	$⊢ \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}) \to y = z)$
38	37	imp	$⊢ (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\})) \to y = z$
39	38	gen2	$⊢ \forall y \forall z ((\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\})) \to y = z)$
40		eqeq1	$⊢ y = z \to (y = \{f \in (M^{ω}) \| f (i) E f (j)\} \leftrightarrow z = \{f \in (M^{ω}) \| f (i) E f (j)\})$
41	40	anbi2d	$⊢ y = z \to ((x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}))$
42	41	2rexbidv	$⊢ y = z \to (\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\}))$
43	42	mo4	$⊢ \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \leftrightarrow \forall y \forall z ((\exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\}) \land \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land z = \{f \in (M^{ω}) \| f (i) E f (j)\})) \to y = z)$
44	39 43	mpbir	$⊢ \exists^{*} y \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})$
45	1 44	mpgbir	$⊢ Fun \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
46		eqid	$⊢ M Sat E = M Sat E$
47	46	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 = \{f \in (M^{ω}) \| f (i) E f (j)\})\}$
48	47	funeqd	$⊢ (M \in V \land E \in W) \to (Fun (M Sat E) (\emptyset) \leftrightarrow Fun \{⟨x, y⟩ \| \exists i \in ω \exists j \in ω (x = i \in_{𝑔} j \land y = \{f \in (M^{ω}) \| f (i) E f (j)\})\})$
49	45 48	mpbiri	$⊢ (M \in V \land E \in W) \to Fun (M Sat E) (\emptyset)$

Metamath Proof Explorer

Theorem satfv0fun

Proof