2ffzoeq - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2ffzoeq		Structured version Visualization version GIF version

Theorem 2ffzoeq 48048

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.)

**Assertion**
Ref	Expression
2ffzoeq	⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))

Distinct variable groups: 𝑖,𝐹 𝑖,𝑀 𝑃,𝑖 Allowed substitution hints: 𝑁(𝑖) 𝑋(𝑖) 𝑌(𝑖)

**Proof of Theorem 2ffzoeq**
Step	Hyp	Ref	Expression
1		eqeq1 2767	. . . . . . . . . . . 12 ⊢ (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅))
2	1	anbi1d 642	. . . . . . . . . . 11 ⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
3		f0bi 6763	. . . . . . . . . . . . 13 ⊢ (𝑃:∅⟶𝑌 ↔ 𝑃 = ∅)
4		ffn 6707	. . . . . . . . . . . . . 14 ⊢ (𝑃:(0..^𝑁)⟶𝑌 → 𝑃 Fn (0..^𝑁))
5		ffn 6707	. . . . . . . . . . . . . 14 ⊢ (𝑃:∅⟶𝑌 → 𝑃 Fn ∅)
6		fndmu 6644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → (0..^𝑁) = ∅)
7		0z 12603	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
8		nn0z 12616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
9	8	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
10		fzon 13711	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
11	7, 9, 10	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
12		nn0ge0 12530	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 0 ≤ 𝑁)
13		0red 11212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ ℝ)
14		nn0re 12514	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	13, 14	letri3d 11353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (0 = 𝑁 ↔ (0 ≤ 𝑁 ∧ 𝑁 ≤ 0)))
16	15	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((0 ≤ 𝑁 ∧ 𝑁 ≤ 0) → 0 = 𝑁))
17	12, 16	mpand 707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 ≤ 0 → 0 = 𝑁))
18	17	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 → 0 = 𝑁))
19	11, 18	sylbird 263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑁) = ∅ → 0 = 𝑁))
20	6, 19	syl5com 32	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁))
21	20	ex 417	. . . . . . . . . . . . . 14 ⊢ (𝑃 Fn (0..^𝑁) → (𝑃 Fn ∅ → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
22	4, 5, 21	syl2imc 42	. . . . . . . . . . . . 13 ⊢ (𝑃:∅⟶𝑌 → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
23	3, 22	sylbir 238	. . . . . . . . . . . 12 ⊢ (𝑃 = ∅ → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
24	23	imp 411	. . . . . . . . . . 11 ⊢ ((𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁))
25	2, 24	biimtrdi 256	. . . . . . . . . 10 ⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
26	25	com3l 90	. . . . . . . . 9 ⊢ ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁)))
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑀 = 0 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁))))
28		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (0..^𝑀) = (0..^0))
29		fzo0 13714	. . . . . . . . . . . 12 ⊢ (0..^0) = ∅
30	28, 29	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (0..^𝑀) = ∅)
31	30	feq2d 6691	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:∅⟶𝑋))
32		f0bi 6763	. . . . . . . . . 10 ⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅)
33	31, 32	bitrdi 290	. . . . . . . . 9 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
34	33	anbi1d 642	. . . . . . . 8 ⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
35		eqeq1 2767	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ 0 = 𝑁))
36	35	imbi2d 343	. . . . . . . . 9 ⊢ (𝑀 = 0 → ((𝐹 = 𝑃 → 𝑀 = 𝑁) ↔ (𝐹 = 𝑃 → 0 = 𝑁)))
37	36	imbi2d 343	. . . . . . . 8 ⊢ (𝑀 = 0 → (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 𝑀 = 𝑁)) ↔ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁))))
38	27, 34, 37	3imtr4d 297	. . . . . . 7 ⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 𝑀 = 𝑁))))
39	38	com3l 90	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁))))
40	39	impcom 412	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁)))
41	40	impcom 412	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 → 𝑀 = 𝑁))
42	28	feq2d 6691	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:(0..^0)⟶𝑋))
43	29	feq2i 6699	. . . . . . . . . . . . 13 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹:∅⟶𝑋)
44	43, 32	bitri 278	. . . . . . . . . . . 12 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹 = ∅)
45	42, 44	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
46	45	adantr 485	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
47		eqeq1 2767	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0))
48	47	biimpac 483	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0)
49		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
50	49	feq2d 6691	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃:(0..^0)⟶𝑌))
51	29	feq2i 6699	. . . . . . . . . . . . 13 ⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃:∅⟶𝑌)
52	51, 3	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃 = ∅)
53	50, 52	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅))
54	48, 53	syl 18	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅))
55	46, 54	anbi12d 643	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃 = ∅)))
56		eqtr3 2785	. . . . . . . . 9 ⊢ ((𝐹 = ∅ ∧ 𝑃 = ∅) → 𝐹 = 𝑃)
57	55, 56	biimtrdi 256	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → 𝐹 = 𝑃))
58	57	com12 33	. . . . . . 7 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝐹 = 𝑃))
59	58	expd 420	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
60	59	adantl 486	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
61	60	impcom 412	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 → 𝐹 = 𝑃))
62	41, 61	impbid 215	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ 𝑀 = 𝑁))
63		ral0 4460	. . . . . 6 ⊢ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)
64	30	raleqdv 3323	. . . . . 6 ⊢ (𝑀 = 0 → (∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)))
65	63, 64	mpbiri 261	. . . . 5 ⊢ (𝑀 = 0 → ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))
66	65	biantrud 540	. . . 4 ⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
67	66	adantr 485	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
68	62, 67	bitrd 282	. 2 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
69		ffn 6707	. . . . . . 7 ⊢ (𝐹:(0..^𝑀)⟶𝑋 → 𝐹 Fn (0..^𝑀))
70	69, 4	anim12i 624	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
71	70	adantl 486	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
72	71	adantl 486	. . . 4 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
73		eqfnfv2 7028	. . . 4 ⊢ ((𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
74	72, 73	syl 18	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
75		df-ne 2959	. . . . . 6 ⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0)
76		elnnne0 12519	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0))
77		0zd 12604	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 ∈ ℤ)
78		nnz 12613	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
79		nngt0 12268	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 < 𝑀)
80	77, 78, 79	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
81	80	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
82		fzoopth 13793	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
83	81, 82	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
84		simpr 489	. . . . . . . . . . . 12 ⊢ ((0 = 0 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁)
85	83, 84	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) → 𝑀 = 𝑁))
86	85	anim1d 622	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
87		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁))
88	87	anim1i 626	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))
89	86, 88	impbid1 228	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
90	89	ex 417	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
91	76, 90	sylbir 238	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0) → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
92	91	impancom 456	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
93	75, 92	biimtrrid 246	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
94	93	adantr 485	. . . 4 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
95	94	impcom 412	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
96	74, 95	bitrd 282	. 2 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
97	68, 96	pm2.61ian 823	1 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∅c0 4287 class class class wbr 5110 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7412 0cc0 11101 < clt 11244 ≤ cle 11245 ℕcn 12234 ℕ₀cn0 12505 ℤcz 12592 ..^cfzo 13684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-n0 12506 df-z 12593 df-uz 12864 df-fz 13537 df-fzo 13685

This theorem is referenced by: (None)

W3C validator