fvmptnn04ifa

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the first case. (Contributed by AV, 10-Nov-2019)

	Ref	Expression
Hypotheses	fvmptnn04if.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, A, if (n = S, C, if (S < n, D, B))))$
	fvmptnn04if.s	$⊢ φ \to S \in ℕ$
	fvmptnn04if.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	fvmptnn04ifa	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to G (N) = ⦋ N / n ⦌ A$

Proof

Step	Hyp	Ref	Expression
1		fvmptnn04if.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, A, if (n = S, C, if (S < n, D, B))))$
2		fvmptnn04if.s	$⊢ φ \to S \in ℕ$
3		fvmptnn04if.n	$⊢ φ \to N \in ℕ_{0}$
4	2	3ad2ant1	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to S \in ℕ$
5	3	3ad2ant1	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to N \in ℕ_{0}$
6		simp3	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to ⦋ N / n ⦌ A \in V$
7		eqidd	$⊢ ((φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \land N = 0) \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ A$
8		simpr	$⊢ (φ \land 0 < N) \to 0 < N$
9	8	gt0ne0d	$⊢ (φ \land 0 < N) \to N \neq 0$
10	9	neneqd	$⊢ (φ \land 0 < N) \to \neg N = 0$
11	10	pm2.21d	$⊢ (φ \land 0 < N) \to (N = 0 \to (N < S \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ B))$
12	11	impancom	$⊢ (φ \land N = 0) \to (0 < N \to (N < S \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ B))$
13	12	3adant3	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to (0 < N \to (N < S \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ B))$
14	13	3imp	$⊢ ((φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \land 0 < N \land N < S) \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ B$
15	2	nnne0d	$⊢ φ \to S \neq 0$
16	15	necomd	$⊢ φ \to 0 \neq S$
17	16	adantr	$⊢ (φ \land N = 0) \to 0 \neq S$
18		neeq1	$⊢ N = 0 \to (N \neq S \leftrightarrow 0 \neq S)$
19	18	adantl	$⊢ (φ \land N = 0) \to (N \neq S \leftrightarrow 0 \neq S)$
20	17 19	mpbird	$⊢ (φ \land N = 0) \to N \neq S$
21	20	3adant3	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to N \neq S$
22	21	neneqd	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to \neg N = S$
23	22	pm2.21d	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to (N = S \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ C)$
24	23	imp	$⊢ ((φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \land N = S) \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ C$
25		nnnn0	$⊢ S \in ℕ \to S \in ℕ_{0}$
26		nn0nlt0	$⊢ S \in ℕ_{0} \to \neg S < 0$
27	2 25 26	3syl	$⊢ φ \to \neg S < 0$
28	27	adantr	$⊢ (φ \land N = 0) \to \neg S < 0$
29		breq2	$⊢ N = 0 \to (S < N \leftrightarrow S < 0)$
30	29	notbid	$⊢ N = 0 \to (\neg S < N \leftrightarrow \neg S < 0)$
31	30	adantl	$⊢ (φ \land N = 0) \to (\neg S < N \leftrightarrow \neg S < 0)$
32	28 31	mpbird	$⊢ (φ \land N = 0) \to \neg S < N$
33	32	3adant3	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to \neg S < N$
34	33	pm2.21d	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to (S < N \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ D)$
35	34	imp	$⊢ ((φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \land S < N) \to ⦋ N / n ⦌ A = ⦋ N / n ⦌ D$
36	1 4 5 6 7 14 24 35	fvmptnn04if	$⊢ (φ \land N = 0 \land ⦋ N / n ⦌ A \in V) \to G (N) = ⦋ N / n ⦌ A$

Metamath Proof Explorer

Theorem fvmptnn04ifa

Proof