2ffzoeq

Description: Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018)

		Ref	Expression
	Assertion	2ffzoeq	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (F = P \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ F = P \to (F = \emptyset \leftrightarrow P = \emptyset)$
2	1	anbi1d	$⊢ F = P \to ((F = \emptyset \land P : (0 ..^N) ⟶ Y) \leftrightarrow (P = \emptyset \land P : (0 ..^N) ⟶ Y))$
3		f0bi	$⊢ P : \emptyset ⟶ Y \leftrightarrow P = \emptyset$
4		ffn	$⊢ P : (0 ..^N) ⟶ Y \to P Fn (0 ..^N)$
5		ffn	$⊢ P : \emptyset ⟶ Y \to P Fn \emptyset$
6		fndmu	$⊢ (P Fn (0 ..^N) \land P Fn \emptyset) \to (0 ..^N) = \emptyset$
7		0z	$⊢ 0 \in ℤ$
8		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
9	8	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℤ$
10		fzon	$⊢ (0 \in ℤ \land N \in ℤ) \to (N \leq 0 \leftrightarrow (0 ..^N) = \emptyset)$
11	7 9 10	sylancr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq 0 \leftrightarrow (0 ..^N) = \emptyset)$
12		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
13		0red	$⊢ N \in ℕ_{0} \to 0 \in ℝ$
14		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
15	13 14	letri3d	$⊢ N \in ℕ_{0} \to (0 = N \leftrightarrow (0 \leq N \land N \leq 0))$
16	15	biimprd	$⊢ N \in ℕ_{0} \to ((0 \leq N \land N \leq 0) \to 0 = N)$
17	12 16	mpand	$⊢ N \in ℕ_{0} \to (N \leq 0 \to 0 = N)$
18	17	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq 0 \to 0 = N)$
19	11 18	sylbird	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((0 ..^N) = \emptyset \to 0 = N)$
20	6 19	syl5com	$⊢ (P Fn (0 ..^N) \land P Fn \emptyset) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N)$
21	20	ex	$⊢ P Fn (0 ..^N) \to (P Fn \emptyset \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N))$
22	4 5 21	syl2imc	$⊢ P : \emptyset ⟶ Y \to (P : (0 ..^N) ⟶ Y \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N))$
23	3 22	sylbir	$⊢ P = \emptyset \to (P : (0 ..^N) ⟶ Y \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N))$
24	23	imp	$⊢ (P = \emptyset \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N)$
25	2 24	syl6bi	$⊢ F = P \to ((F = \emptyset \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 = N))$
26	25	com3l	$⊢ (F = \emptyset \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (F = P \to 0 = N))$
27	26	a1i	$⊢ M = 0 \to ((F = \emptyset \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (F = P \to 0 = N)))$
28		oveq2	$⊢ M = 0 \to (0 ..^M) = (0 ..^0)$
29		fzo0	$⊢ (0 ..^0) = \emptyset$
30	28 29	eqtrdi	$⊢ M = 0 \to (0 ..^M) = \emptyset$
31	30	feq2d	$⊢ M = 0 \to (F : (0 ..^M) ⟶ X \leftrightarrow F : \emptyset ⟶ X)$
32		f0bi	$⊢ F : \emptyset ⟶ X \leftrightarrow F = \emptyset$
33	31 32	bitrdi	$⊢ M = 0 \to (F : (0 ..^M) ⟶ X \leftrightarrow F = \emptyset)$
34	33	anbi1d	$⊢ M = 0 \to ((F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \leftrightarrow (F = \emptyset \land P : (0 ..^N) ⟶ Y))$
35		eqeq1	$⊢ M = 0 \to (M = N \leftrightarrow 0 = N)$
36	35	imbi2d	$⊢ M = 0 \to ((F = P \to M = N) \leftrightarrow (F = P \to 0 = N))$
37	36	imbi2d	$⊢ M = 0 \to (((M \in ℕ_{0} \land N \in ℕ_{0}) \to (F = P \to M = N)) \leftrightarrow ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (F = P \to 0 = N)))$
38	27 34 37	3imtr4d	$⊢ M = 0 \to ((F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (F = P \to M = N)))$
39	38	com3l	$⊢ (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (M = 0 \to (F = P \to M = N)))$
40	39	impcom	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (M = 0 \to (F = P \to M = N))$
41	40	impcom	$⊢ (M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F = P \to M = N)$
42	28	feq2d	$⊢ M = 0 \to (F : (0 ..^M) ⟶ X \leftrightarrow F : (0 ..^0) ⟶ X)$
43	29	feq2i	$⊢ F : (0 ..^0) ⟶ X \leftrightarrow F : \emptyset ⟶ X$
44	43 32	bitri	$⊢ F : (0 ..^0) ⟶ X \leftrightarrow F = \emptyset$
45	42 44	bitrdi	$⊢ M = 0 \to (F : (0 ..^M) ⟶ X \leftrightarrow F = \emptyset)$
46	45	adantr	$⊢ (M = 0 \land M = N) \to (F : (0 ..^M) ⟶ X \leftrightarrow F = \emptyset)$
47		eqeq1	$⊢ M = N \to (M = 0 \leftrightarrow N = 0)$
48	47	biimpac	$⊢ (M = 0 \land M = N) \to N = 0$
49		oveq2	$⊢ N = 0 \to (0 ..^N) = (0 ..^0)$
50	49	feq2d	$⊢ N = 0 \to (P : (0 ..^N) ⟶ Y \leftrightarrow P : (0 ..^0) ⟶ Y)$
51	29	feq2i	$⊢ P : (0 ..^0) ⟶ Y \leftrightarrow P : \emptyset ⟶ Y$
52	51 3	bitri	$⊢ P : (0 ..^0) ⟶ Y \leftrightarrow P = \emptyset$
53	50 52	bitrdi	$⊢ N = 0 \to (P : (0 ..^N) ⟶ Y \leftrightarrow P = \emptyset)$
54	48 53	syl	$⊢ (M = 0 \land M = N) \to (P : (0 ..^N) ⟶ Y \leftrightarrow P = \emptyset)$
55	46 54	anbi12d	$⊢ (M = 0 \land M = N) \to ((F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \leftrightarrow (F = \emptyset \land P = \emptyset))$
56		eqtr3	$⊢ (F = \emptyset \land P = \emptyset) \to F = P$
57	55 56	syl6bi	$⊢ (M = 0 \land M = N) \to ((F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to F = P)$
58	57	com12	$⊢ (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to ((M = 0 \land M = N) \to F = P)$
59	58	expd	$⊢ (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to (M = 0 \to (M = N \to F = P))$
60	59	adantl	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (M = 0 \to (M = N \to F = P))$
61	60	impcom	$⊢ (M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (M = N \to F = P)$
62	41 61	impbid	$⊢ (M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F = P \leftrightarrow M = N)$
63		ral0	$⊢ \forall i \in \emptyset F (i) = P (i)$
64	30	raleqdv	$⊢ M = 0 \to (\forall i \in (0 ..^M) F (i) = P (i) \leftrightarrow \forall i \in \emptyset F (i) = P (i))$
65	63 64	mpbiri	$⊢ M = 0 \to \forall i \in (0 ..^M) F (i) = P (i)$
66	65	biantrud	$⊢ M = 0 \to (M = N \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
67	66	adantr	$⊢ (M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (M = N \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
68	62 67	bitrd	$⊢ (M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F = P \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
69		ffn	$⊢ F : (0 ..^M) ⟶ X \to F Fn (0 ..^M)$
70	69 4	anim12i	$⊢ (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y) \to (F Fn (0 ..^M) \land P Fn (0 ..^N))$
71	70	adantl	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (F Fn (0 ..^M) \land P Fn (0 ..^N))$
72	71	adantl	$⊢ (\neg M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F Fn (0 ..^M) \land P Fn (0 ..^N))$
73		eqfnfv2	$⊢ (F Fn (0 ..^M) \land P Fn (0 ..^N)) \to (F = P \leftrightarrow ((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)))$
74	72 73	syl	$⊢ (\neg M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F = P \leftrightarrow ((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)))$
75		df-ne	$⊢ M \neq 0 \leftrightarrow \neg M = 0$
76		elnnne0	$⊢ M \in ℕ \leftrightarrow (M \in ℕ_{0} \land M \neq 0)$
77		0zd	$⊢ M \in ℕ \to 0 \in ℤ$
78		nnz	$⊢ M \in ℕ \to M \in ℤ$
79		nngt0	$⊢ M \in ℕ \to 0 < M$
80	77 78 79	3jca	$⊢ M \in ℕ \to (0 \in ℤ \land M \in ℤ \land 0 < M)$
81	80	adantr	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to (0 \in ℤ \land M \in ℤ \land 0 < M)$
82		fzoopth	$⊢ (0 \in ℤ \land M \in ℤ \land 0 < M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow (0 = 0 \land M = N))$
83	81 82	syl	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to ((0 ..^M) = (0 ..^N) \leftrightarrow (0 = 0 \land M = N))$
84		simpr	$⊢ (0 = 0 \land M = N) \to M = N$
85	83 84	syl6bi	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to ((0 ..^M) = (0 ..^N) \to M = N)$
86	85	anim1d	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \to (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
87		oveq2	$⊢ M = N \to (0 ..^M) = (0 ..^N)$
88	87	anim1i	$⊢ (M = N \land \forall i \in (0 ..^M) F (i) = P (i)) \to ((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i))$
89	86 88	impbid1	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
90	89	ex	$⊢ M \in ℕ \to (N \in ℕ_{0} \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i))))$
91	76 90	sylbir	$⊢ (M \in ℕ_{0} \land M \neq 0) \to (N \in ℕ_{0} \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i))))$
92	91	impancom	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \neq 0 \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i))))$
93	75 92	syl5bir	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg M = 0 \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i))))$
94	93	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (\neg M = 0 \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i))))$
95	94	impcom	$⊢ (\neg M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (((0 ..^M) = (0 ..^N) \land \forall i \in (0 ..^M) F (i) = P (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
96	74 95	bitrd	$⊢ (\neg M = 0 \land ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y))) \to (F = P \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$
97	68 96	pm2.61ian	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (F : (0 ..^M) ⟶ X \land P : (0 ..^N) ⟶ Y)) \to (F = P \leftrightarrow (M = N \land \forall i \in (0 ..^M) F (i) = P (i)))$

Metamath Proof Explorer

Theorem 2ffzoeq

Proof