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 47364

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 2735	. . . . . . . . . . . 12 ⊢ (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅))
2	1	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
3		f0bi 6706	. . . . . . . . . . . . 13 ⊢ (𝑃:∅⟶𝑌 ↔ 𝑃 = ∅)
4		ffn 6651	. . . . . . . . . . . . . 14 ⊢ (𝑃:(0..^𝑁)⟶𝑌 → 𝑃 Fn (0..^𝑁))
5		ffn 6651	. . . . . . . . . . . . . 14 ⊢ (𝑃:∅⟶𝑌 → 𝑃 Fn ∅)
6		fndmu 6588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → (0..^𝑁) = ∅)
7		0z 12479	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
8		nn0z 12493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
9	8	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
10		fzon 13580	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
11	7, 9, 10	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
12		nn0ge0 12406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → 0 ≤ 𝑁)
13		0red 11115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ ℝ)
14		nn0re 12390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
15	13, 14	letri3d 11255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (0 = 𝑁 ↔ (0 ≤ 𝑁 ∧ 𝑁 ≤ 0)))
16	15	biimprd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((0 ≤ 𝑁 ∧ 𝑁 ≤ 0) → 0 = 𝑁))
17	12, 16	mpand 695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 ≤ 0 → 0 = 𝑁))
18	17	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 0 → 0 = 𝑁))
19	11, 18	sylbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑁) = ∅ → 0 = 𝑁))
20	6, 19	syl5com 31	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁))
21	20	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑃 Fn (0..^𝑁) → (𝑃 Fn ∅ → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
22	4, 5, 21	syl2imc 41	. . . . . . . . . . . . 13 ⊢ (𝑃:∅⟶𝑌 → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
23	3, 22	sylbir 235	. . . . . . . . . . . 12 ⊢ (𝑃 = ∅ → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
24	23	imp 406	. . . . . . . . . . 11 ⊢ ((𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁))
25	2, 24	biimtrdi 253	. . . . . . . . . 10 ⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 = 𝑁)))
26	25	com3l 89	. . . . . . . . 9 ⊢ ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁)))
27	26	a1i 11	. . . . . . . 8 ⊢ (𝑀 = 0 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁))))
28		oveq2 7354	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (0..^𝑀) = (0..^0))
29		fzo0 13583	. . . . . . . . . . . 12 ⊢ (0..^0) = ∅
30	28, 29	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (0..^𝑀) = ∅)
31	30	feq2d 6635	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:∅⟶𝑋))
32		f0bi 6706	. . . . . . . . . 10 ⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅)
33	31, 32	bitrdi 287	. . . . . . . . 9 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
34	33	anbi1d 631	. . . . . . . 8 ⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
35		eqeq1 2735	. . . . . . . . . 10 ⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ 0 = 𝑁))
36	35	imbi2d 340	. . . . . . . . 9 ⊢ (𝑀 = 0 → ((𝐹 = 𝑃 → 𝑀 = 𝑁) ↔ (𝐹 = 𝑃 → 0 = 𝑁)))
37	36	imbi2d 340	. . . . . . . 8 ⊢ (𝑀 = 0 → (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 𝑀 = 𝑁)) ↔ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 0 = 𝑁))))
38	27, 34, 37	3imtr4d 294	. . . . . . 7 ⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐹 = 𝑃 → 𝑀 = 𝑁))))
39	38	com3l 89	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁))))
40	39	impcom 407	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁)))
41	40	impcom 407	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 → 𝑀 = 𝑁))
42	28	feq2d 6635	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:(0..^0)⟶𝑋))
43	29	feq2i 6643	. . . . . . . . . . . . 13 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹:∅⟶𝑋)
44	43, 32	bitri 275	. . . . . . . . . . . 12 ⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹 = ∅)
45	42, 44	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
46	45	adantr 480	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅))
47		eqeq1 2735	. . . . . . . . . . . 12 ⊢ (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0))
48	47	biimpac 478	. . . . . . . . . . 11 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0)
49		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0))
50	49	feq2d 6635	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃:(0..^0)⟶𝑌))
51	29	feq2i 6643	. . . . . . . . . . . . 13 ⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃:∅⟶𝑌)
52	51, 3	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃 = ∅)
53	50, 52	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅))
54	48, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅))
55	46, 54	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃 = ∅)))
56		eqtr3 2753	. . . . . . . . 9 ⊢ ((𝐹 = ∅ ∧ 𝑃 = ∅) → 𝐹 = 𝑃)
57	55, 56	biimtrdi 253	. . . . . . . 8 ⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → 𝐹 = 𝑃))
58	57	com12 32	. . . . . . 7 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝐹 = 𝑃))
59	58	expd 415	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
60	59	adantl 481	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃)))
61	60	impcom 407	. . . 4 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 → 𝐹 = 𝑃))
62	41, 61	impbid 212	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ 𝑀 = 𝑁))
63		ral0 4463	. . . . . 6 ⊢ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)
64	30	raleqdv 3292	. . . . . 6 ⊢ (𝑀 = 0 → (∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖)))
65	63, 64	mpbiri 258	. . . . 5 ⊢ (𝑀 = 0 → ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))
66	65	biantrud 531	. . . 4 ⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
67	66	adantr 480	. . 3 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
68	62, 67	bitrd 279	. 2 ⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
69		ffn 6651	. . . . . . 7 ⊢ (𝐹:(0..^𝑀)⟶𝑋 → 𝐹 Fn (0..^𝑀))
70	69, 4	anim12i 613	. . . . . 6 ⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
71	70	adantl 481	. . . . 5 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
72	71	adantl 481	. . . 4 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
73		eqfnfv2 6965	. . . 4 ⊢ ((𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
74	72, 73	syl 17	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
75		df-ne 2929	. . . . . 6 ⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0)
76		elnnne0 12395	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0))
77		0zd 12480	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 ∈ ℤ)
78		nnz 12489	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
79		nngt0 12156	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → 0 < 𝑀)
80	77, 78, 79	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
81	80	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
82		fzoopth 13662	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
83	81, 82	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
84		simpr 484	. . . . . . . . . . . 12 ⊢ ((0 = 0 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁)
85	83, 84	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((0..^𝑀) = (0..^𝑁) → 𝑀 = 𝑁))
86	85	anim1d 611	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
87		oveq2 7354	. . . . . . . . . . 11 ⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁))
88	87	anim1i 615	. . . . . . . . . 10 ⊢ ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))
89	86, 88	impbid1 225	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
90	89	ex 412	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
91	76, 90	sylbir 235	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑀 ≠ 0) → (𝑁 ∈ ℕ₀ → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
92	91	impancom 451	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
93	75, 92	biimtrrid 243	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
94	93	adantr 480	. . . 4 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))))
95	94	impcom 407	. . 3 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
96	74, 95	bitrd 279	. 2 ⊢ ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
97	68, 96	pm2.61ian 811	1 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∅c0 4283 class class class wbr 5091 Fn wfn 6476 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 0cc0 11006 < clt 11146 ≤ cle 11147 ℕcn 12125 ℕ₀cn0 12381 ℤcz 12468 ..^cfzo 13554

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-fzo 13555

This theorem is referenced by: (None)

W3C validator