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 48492

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 2764	. . . . . . . . . . . 12 ⊢ (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅))
2	1	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
3		f0bi 6766	. . . . . . . . . . . . 13 ⊢ (𝑃:∅⟶𝑌 ↔ 𝑃 = ∅)
4		ffn 6710	. . . . . . . . . . . . . 14 ⊢ (𝑃:(0..^𝑁)⟶𝑌 → 𝑃 Fn (0..^𝑁))
5		ffn 6710	. . . . . . . . . . . . . 14 ⊢ (𝑃:∅⟶𝑌 → 𝑃 Fn ∅)
6		fndmu 6647	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → (0..^𝑁) = ∅)
7		0z 12708	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
8		nn0z 12721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
9	8	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
10		fzon 13819	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
11	7, 9, 10	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
12		nn0ge0 12635	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 0 ≤ 𝑁)
13		0red 11315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ ℝ)
14		nn0re 12619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	13, 14	letri3d 11456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (0 = 𝑁 ↔ (0 ≤ 𝑁 ∧ 𝑁 ≤ 0)))
16	15	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((0 ≤ 𝑁 ∧ 𝑁 ≤ 0) → 0 = 𝑁))
17	12, 16	mpand 708	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 ≤ 0 → 0 = 𝑁))
18	17	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 → 0 = 𝑁))
19	11, 18	sylbird 263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑁) = ∅ → 0 = 𝑁))
20	6, 19	syl5com 32	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁))
21	20	ex 418	. . . . . . . . . . . . . 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 412	. . . . . . . . . . 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 7429	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (0..^𝑀) = (0..^0))
29		fzo0 13822	. . . . . . . . . . . 12 ⊢ (0..^0) = ∅
30	28, 29	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (0..^𝑀) = ∅)
31	30	feq2d 6694	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:∅⟶𝑋))
32		f0bi 6766	. . . . . . . . . 10 ⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅)
33	31, 32	bitrdi 290	. . . . . . . . 9 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
34	33	anbi1d 643	. . . . . . . 8 ⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
35		eqeq1 2764	. . . . . . . . . 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 413	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁)))
41	40	impcom 413	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 → 𝑀 = 𝑁))
42	28	feq2d 6694	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:(0..^0)⟶𝑋))
43	29	feq2i 6702	. . . . . . . . . . . . 13 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹:∅⟶𝑋)
44	43, 32	bitri 278	. . . . . . . . . . . 12 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹 = ∅)
45	42, 44	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
46	45	adantr 486	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
47		eqeq1 2764	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0))
48	47	biimpac 484	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0)
49		oveq2 7429	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
50	49	feq2d 6694	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃:(0..^0)⟶𝑌))
51	29	feq2i 6702	. . . . . . . . . . . . 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 644	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃 = ∅)))
56		eqtr3 2782	. . . . . . . . 9 ⊢ ((𝐹 = ∅ ∧ 𝑃 = ∅) → 𝐹 = 𝑃)
57	55, 56	biimtrdi 256	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → 𝐹 = 𝑃))
58	57	com12 33	. . . . . . 7 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝐹 = 𝑃))
59	58	expd 421	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
60	59	adantl 487	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
61	60	impcom 413	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 → 𝐹 = 𝑃))
62	41, 61	impbid 215	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ 𝑀 = 𝑁))
63		ral0 4453	. . . . . 6 ⊢ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)
64	30	raleqdv 3319	. . . . . 6 ⊢ (𝑀 = 0 → (∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)))
65	63, 64	mpbiri 261	. . . . 5 ⊢ (𝑀 = 0 → ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))
66	65	biantrud 541	. . . 4 ⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
67	66	adantr 486	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
68	62, 67	bitrd 282	. 2 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
69		ffn 6710	. . . . . . 7 ⊢ (𝐹:(0..^𝑀)⟶𝑋 → 𝐹 Fn (0..^𝑀))
70	69, 4	anim12i 625	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
71	70	adantl 487	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
72	71	adantl 487	. . . 4 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
73		eqfnfv2 7031	. . . 4 ⊢ ((𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
74	72, 73	syl 18	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
75		df-ne 2956	. . . . . 6 ⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0)
76		elnnne0 12624	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0))
77		0zd 12709	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 ∈ ℤ)
78		nnz 12718	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
79		nngt0 12373	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 < 𝑀)
80	77, 78, 79	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
81	80	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
82		fzoopth 13901	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
83	81, 82	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
84		simpr 490	. . . . . . . . . . . 12 ⊢ ((0 = 0 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁)
85	83, 84	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) → 𝑀 = 𝑁))
86	85	anim1d 623	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
87		oveq2 7429	. . . . . . . . . . 11 ⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁))
88	87	anim1i 627	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))
89	86, 88	impbid1 228	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
90	89	ex 418	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
91	76, 90	sylbir 238	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0) → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
92	91	impancom 457	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
93	75, 92	biimtrrid 246	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
94	93	adantr 486	. . . 4 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
95	94	impcom 413	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
96	74, 95	bitrd 282	. 2 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
97	68, 96	pm2.61ian 824	1 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∅c0 4278 class class class wbr 5102 Fn wfn 6534 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 0cc0 11204 < clt 11347 ≤ cle 11348 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ..^cfzo 13792

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-n0 12611 df-z 12698 df-uz 12970 df-fz 13644 df-fzo 13793

This theorem is used by: (None)

W3C validator