satffun

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

		Ref	Expression
	Assertion	satffun	$⊢ (M \in V \land E \in W \land N \in ω) \to Fun (M Sat E) (N)$

Proof

Step	Hyp	Ref	Expression
1		satfv0fun	$⊢ (M \in V \land E \in W) \to Fun (M Sat E) (\emptyset)$
2	1	3adant3	$⊢ (M \in V \land E \in W \land N \in ω) \to Fun (M Sat E) (\emptyset)$
3		fveq2	$⊢ N = \emptyset \to (M Sat E) (N) = (M Sat E) (\emptyset)$
4	3	funeqd	$⊢ N = \emptyset \to (Fun (M Sat E) (N) \leftrightarrow Fun (M Sat E) (\emptyset))$
5	2 4	syl5ibr	$⊢ N = \emptyset \to ((M \in V \land E \in W \land N \in ω) \to Fun (M Sat E) (N))$
6		df-ne	$⊢ N \neq \emptyset \leftrightarrow \neg N = \emptyset$
7		nnsuc	$⊢ (N \in ω \land N \neq \emptyset) \to \exists n \in ω N = suc n$
8		suceq	$⊢ x = \emptyset \to suc x = suc \emptyset$
9	8	fveq2d	$⊢ x = \emptyset \to (M Sat E) (suc x) = (M Sat E) (suc \emptyset)$
10	9	funeqd	$⊢ x = \emptyset \to (Fun (M Sat E) (suc x) \leftrightarrow Fun (M Sat E) (suc \emptyset))$
11	10	imbi2d	$⊢ x = \emptyset \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc x)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc \emptyset)))$
12		suceq	$⊢ x = y \to suc x = suc y$
13	12	fveq2d	$⊢ x = y \to (M Sat E) (suc x) = (M Sat E) (suc y)$
14	13	funeqd	$⊢ x = y \to (Fun (M Sat E) (suc x) \leftrightarrow Fun (M Sat E) (suc y))$
15	14	imbi2d	$⊢ x = y \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc x)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc y)))$
16		suceq	$⊢ x = suc y \to suc x = suc suc y$
17	16	fveq2d	$⊢ x = suc y \to (M Sat E) (suc x) = (M Sat E) (suc suc y)$
18	17	funeqd	$⊢ x = suc y \to (Fun (M Sat E) (suc x) \leftrightarrow Fun (M Sat E) (suc suc y))$
19	18	imbi2d	$⊢ x = suc y \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc x)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc suc y)))$
20		suceq	$⊢ x = n \to suc x = suc n$
21	20	fveq2d	$⊢ x = n \to (M Sat E) (suc x) = (M Sat E) (suc n)$
22	21	funeqd	$⊢ x = n \to (Fun (M Sat E) (suc x) \leftrightarrow Fun (M Sat E) (suc n))$
23	22	imbi2d	$⊢ x = n \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc x)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc n)))$
24		satffunlem1	$⊢ (M \in V \land E \in W) \to Fun (M Sat E) (suc \emptyset)$
25		pm2.27	$⊢ (M \in V \land E \in W) \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc y)) \to Fun (M Sat E) (suc y))$
26		satffunlem2	$⊢ (y \in ω \land (M \in V \land E \in W)) \to (Fun (M Sat E) (suc y) \to Fun (M Sat E) (suc suc y))$
27	26	expcom	$⊢ (M \in V \land E \in W) \to (y \in ω \to (Fun (M Sat E) (suc y) \to Fun (M Sat E) (suc suc y)))$
28	27	com23	$⊢ (M \in V \land E \in W) \to (Fun (M Sat E) (suc y) \to (y \in ω \to Fun (M Sat E) (suc suc y)))$
29	25 28	syld	$⊢ (M \in V \land E \in W) \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc y)) \to (y \in ω \to Fun (M Sat E) (suc suc y)))$
30	29	com13	$⊢ y \in ω \to (((M \in V \land E \in W) \to Fun (M Sat E) (suc y)) \to ((M \in V \land E \in W) \to Fun (M Sat E) (suc suc y)))$
31	11 15 19 23 24 30	finds	$⊢ n \in ω \to ((M \in V \land E \in W) \to Fun (M Sat E) (suc n))$
32	31	adantr	$⊢ (n \in ω \land N = suc n) \to ((M \in V \land E \in W) \to Fun (M Sat E) (suc n))$
33		fveq2	$⊢ N = suc n \to (M Sat E) (N) = (M Sat E) (suc n)$
34	33	funeqd	$⊢ N = suc n \to (Fun (M Sat E) (N) \leftrightarrow Fun (M Sat E) (suc n))$
35	34	imbi2d	$⊢ N = suc n \to (((M \in V \land E \in W) \to Fun (M Sat E) (N)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc n)))$
36	35	adantl	$⊢ (n \in ω \land N = suc n) \to (((M \in V \land E \in W) \to Fun (M Sat E) (N)) \leftrightarrow ((M \in V \land E \in W) \to Fun (M Sat E) (suc n)))$
37	32 36	mpbird	$⊢ (n \in ω \land N = suc n) \to ((M \in V \land E \in W) \to Fun (M Sat E) (N))$
38	37	rexlimiva	$⊢ \exists n \in ω N = suc n \to ((M \in V \land E \in W) \to Fun (M Sat E) (N))$
39	7 38	syl	$⊢ (N \in ω \land N \neq \emptyset) \to ((M \in V \land E \in W) \to Fun (M Sat E) (N))$
40	39	expcom	$⊢ N \neq \emptyset \to (N \in ω \to ((M \in V \land E \in W) \to Fun (M Sat E) (N)))$
41	6 40	sylbir	$⊢ \neg N = \emptyset \to (N \in ω \to ((M \in V \land E \in W) \to Fun (M Sat E) (N)))$
42	41	com13	$⊢ (M \in V \land E \in W) \to (N \in ω \to (\neg N = \emptyset \to Fun (M Sat E) (N)))$
43	42	3impia	$⊢ (M \in V \land E \in W \land N \in ω) \to (\neg N = \emptyset \to Fun (M Sat E) (N))$
44	43	com12	$⊢ \neg N = \emptyset \to ((M \in V \land E \in W \land N \in ω) \to Fun (M Sat E) (N))$
45	5 44	pm2.61i	$⊢ (M \in V \land E \in W \land N \in ω) \to Fun (M Sat E) (N)$

Metamath Proof Explorer

Theorem satffun

Proof