Users' Mathboxes 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 47339
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..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
Distinct variable groups:   𝑖,𝐹   𝑖,𝑀   𝑃,𝑖
Allowed substitution hints:   𝑁(𝑖)   𝑋(𝑖)   𝑌(𝑖)

Proof of Theorem 2ffzoeq
StepHypRef Expression
1 eqeq1 2741 . . . . . . . . . . . 12 (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅))
21anbi1d 631 . . . . . . . . . . 11 (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
3 f0bi 6791 . . . . . . . . . . . . 13 (𝑃:∅⟶𝑌𝑃 = ∅)
4 ffn 6736 . . . . . . . . . . . . . 14 (𝑃:(0..^𝑁)⟶𝑌𝑃 Fn (0..^𝑁))
5 ffn 6736 . . . . . . . . . . . . . 14 (𝑃:∅⟶𝑌𝑃 Fn ∅)
6 fndmu 6675 . . . . . . . . . . . . . . . 16 ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → (0..^𝑁) = ∅)
7 0z 12624 . . . . . . . . . . . . . . . . . 18 0 ∈ ℤ
8 nn0z 12638 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
98adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
10 fzon 13720 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
117, 9, 10sylancr 587 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅))
12 nn0ge0 12551 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
13 0red 11264 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 0 ∈ ℝ)
14 nn0re 12535 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
1513, 14letri3d 11403 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (0 = 𝑁 ↔ (0 ≤ 𝑁𝑁 ≤ 0)))
1615biimprd 248 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0 → ((0 ≤ 𝑁𝑁 ≤ 0) → 0 = 𝑁))
1712, 16mpand 695 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (𝑁 ≤ 0 → 0 = 𝑁))
1817adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ≤ 0 → 0 = 𝑁))
1911, 18sylbird 260 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((0..^𝑁) = ∅ → 0 = 𝑁))
206, 19syl5com 31 . . . . . . . . . . . . . . 15 ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁))
2120ex 412 . . . . . . . . . . . . . 14 (𝑃 Fn (0..^𝑁) → (𝑃 Fn ∅ → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁)))
224, 5, 21syl2imc 41 . . . . . . . . . . . . 13 (𝑃:∅⟶𝑌 → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁)))
233, 22sylbir 235 . . . . . . . . . . . 12 (𝑃 = ∅ → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁)))
2423imp 406 . . . . . . . . . . 11 ((𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁))
252, 24biimtrdi 253 . . . . . . . . . 10 (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 0 = 𝑁)))
2625com3l 89 . . . . . . . . 9 ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐹 = 𝑃 → 0 = 𝑁)))
2726a1i 11 . . . . . . . 8 (𝑀 = 0 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐹 = 𝑃 → 0 = 𝑁))))
28 oveq2 7439 . . . . . . . . . . . 12 (𝑀 = 0 → (0..^𝑀) = (0..^0))
29 fzo0 13723 . . . . . . . . . . . 12 (0..^0) = ∅
3028, 29eqtrdi 2793 . . . . . . . . . . 11 (𝑀 = 0 → (0..^𝑀) = ∅)
3130feq2d 6722 . . . . . . . . . 10 (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋𝐹:∅⟶𝑋))
32 f0bi 6791 . . . . . . . . . 10 (𝐹:∅⟶𝑋𝐹 = ∅)
3331, 32bitrdi 287 . . . . . . . . 9 (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋𝐹 = ∅))
3433anbi1d 631 . . . . . . . 8 (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌)))
35 eqeq1 2741 . . . . . . . . . 10 (𝑀 = 0 → (𝑀 = 𝑁 ↔ 0 = 𝑁))
3635imbi2d 340 . . . . . . . . 9 (𝑀 = 0 → ((𝐹 = 𝑃𝑀 = 𝑁) ↔ (𝐹 = 𝑃 → 0 = 𝑁)))
3736imbi2d 340 . . . . . . . 8 (𝑀 = 0 → (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐹 = 𝑃𝑀 = 𝑁)) ↔ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐹 = 𝑃 → 0 = 𝑁))))
3827, 34, 373imtr4d 294 . . . . . . 7 (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐹 = 𝑃𝑀 = 𝑁))))
3938com3l 89 . . . . . 6 ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 = 0 → (𝐹 = 𝑃𝑀 = 𝑁))))
4039impcom 407 . . . . 5 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝐹 = 𝑃𝑀 = 𝑁)))
4140impcom 407 . . . 4 ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃𝑀 = 𝑁))
4228feq2d 6722 . . . . . . . . . . . 12 (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋𝐹:(0..^0)⟶𝑋))
4329feq2i 6728 . . . . . . . . . . . . 13 (𝐹:(0..^0)⟶𝑋𝐹:∅⟶𝑋)
4443, 32bitri 275 . . . . . . . . . . . 12 (𝐹:(0..^0)⟶𝑋𝐹 = ∅)
4542, 44bitrdi 287 . . . . . . . . . . 11 (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋𝐹 = ∅))
4645adantr 480 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝐹:(0..^𝑀)⟶𝑋𝐹 = ∅))
47 eqeq1 2741 . . . . . . . . . . . 12 (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0))
4847biimpac 478 . . . . . . . . . . 11 ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0)
49 oveq2 7439 . . . . . . . . . . . . 13 (𝑁 = 0 → (0..^𝑁) = (0..^0))
5049feq2d 6722 . . . . . . . . . . . 12 (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌𝑃:(0..^0)⟶𝑌))
5129feq2i 6728 . . . . . . . . . . . . 13 (𝑃:(0..^0)⟶𝑌𝑃:∅⟶𝑌)
5251, 3bitri 275 . . . . . . . . . . . 12 (𝑃:(0..^0)⟶𝑌𝑃 = ∅)
5350, 52bitrdi 287 . . . . . . . . . . 11 (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌𝑃 = ∅))
5448, 53syl 17 . . . . . . . . . 10 ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝑃:(0..^𝑁)⟶𝑌𝑃 = ∅))
5546, 54anbi12d 632 . . . . . . . . 9 ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃 = ∅)))
56 eqtr3 2763 . . . . . . . . 9 ((𝐹 = ∅ ∧ 𝑃 = ∅) → 𝐹 = 𝑃)
5755, 56biimtrdi 253 . . . . . . . 8 ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → 𝐹 = 𝑃))
5857com12 32 . . . . . . 7 ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝐹 = 𝑃))
5958expd 415 . . . . . 6 ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → (𝑀 = 0 → (𝑀 = 𝑁𝐹 = 𝑃)))
6059adantl 481 . . . . 5 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁𝐹 = 𝑃)))
6160impcom 407 . . . 4 ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁𝐹 = 𝑃))
6241, 61impbid 212 . . 3 ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃𝑀 = 𝑁))
63 ral0 4513 . . . . . 6 𝑖 ∈ ∅ (𝐹𝑖) = (𝑃𝑖)
6430raleqdv 3326 . . . . . 6 (𝑀 = 0 → (∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖) ↔ ∀𝑖 ∈ ∅ (𝐹𝑖) = (𝑃𝑖)))
6563, 64mpbiri 258 . . . . 5 (𝑀 = 0 → ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))
6665biantrud 531 . . . 4 (𝑀 = 0 → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
6766adantr 480 . . 3 ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
6862, 67bitrd 279 . 2 ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
69 ffn 6736 . . . . . . 7 (𝐹:(0..^𝑀)⟶𝑋𝐹 Fn (0..^𝑀))
7069, 4anim12i 613 . . . . . 6 ((𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
7170adantl 481 . . . . 5 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
7271adantl 481 . . . 4 ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)))
73 eqfnfv2 7052 . . . 4 ((𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
7472, 73syl 17 . . 3 ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
75 df-ne 2941 . . . . . 6 (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0)
76 elnnne0 12540 . . . . . . . 8 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0𝑀 ≠ 0))
77 0zd 12625 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 0 ∈ ℤ)
78 nnz 12634 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
79 nngt0 12297 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 0 < 𝑀)
8077, 78, 793jca 1129 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
8180adantr 480 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
82 fzoopth 13801 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
8381, 82syl 17 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
84 simpr 484 . . . . . . . . . . . 12 ((0 = 0 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁)
8583, 84biimtrdi 253 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((0..^𝑀) = (0..^𝑁) → 𝑀 = 𝑁))
8685anim1d 611 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
87 oveq2 7439 . . . . . . . . . . 11 (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁))
8887anim1i 615 . . . . . . . . . 10 ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))
8986, 88impbid1 225 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
9089ex 412 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑁 ∈ ℕ0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))))
9176, 90sylbir 235 . . . . . . 7 ((𝑀 ∈ ℕ0𝑀 ≠ 0) → (𝑁 ∈ ℕ0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))))
9291impancom 451 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))))
9375, 92biimtrrid 243 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))))
9493adantr 480 . . . 4 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)))))
9594impcom 407 . . 3 ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
9674, 95bitrd 279 . 2 ((¬ 𝑀 = 0 ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
9768, 96pm2.61ian 812 1 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹𝑖) = (𝑃𝑖))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  c0 4333   class class class wbr 5143   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  0cc0 11155   < clt 11295  cle 11296  cn 12266  0cn0 12526  cz 12613  ..^cfzo 13694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator