Proof of Theorem 2ffzoeq
Step | Hyp | Ref
| Expression |
1 | | eqeq1 2743 |
. . . . . . . . . . . 12
⊢ (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅)) |
2 | 1 | anbi1d 629 |
. . . . . . . . . . 11
⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌))) |
3 | | f0bi 6653 |
. . . . . . . . . . . . 13
⊢ (𝑃:∅⟶𝑌 ↔ 𝑃 = ∅) |
4 | | ffn 6596 |
. . . . . . . . . . . . . 14
⊢ (𝑃:(0..^𝑁)⟶𝑌 → 𝑃 Fn (0..^𝑁)) |
5 | | ffn 6596 |
. . . . . . . . . . . . . 14
⊢ (𝑃:∅⟶𝑌 → 𝑃 Fn ∅) |
6 | | fndmu 6536 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → (0..^𝑁) = ∅) |
7 | | 0z 12313 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ |
8 | | nn0z 12326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℤ) |
10 | | fzon 13389 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (𝑁
≤ 0 ↔ (0..^𝑁) =
∅)) |
11 | 7, 9, 10 | sylancr 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅)) |
12 | | nn0ge0 12241 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
13 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ ℝ) |
14 | | nn0re 12225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
15 | 13, 14 | letri3d 11100 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (0 = 𝑁 ↔ (0
≤ 𝑁 ∧ 𝑁 ≤ 0))) |
16 | 15 | biimprd 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((0 ≤ 𝑁 ∧
𝑁 ≤ 0) → 0 = 𝑁)) |
17 | 12, 16 | mpand 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ≤ 0 → 0 =
𝑁)) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 0 → 0 = 𝑁)) |
19 | 11, 18 | sylbird 259 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0..^𝑁) = ∅ → 0 = 𝑁)) |
20 | 6, 19 | syl5com 31 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 Fn (0..^𝑁) ∧ 𝑃 Fn ∅) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁)) |
21 | 20 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑃 Fn (0..^𝑁) → (𝑃 Fn ∅ → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁))) |
22 | 4, 5, 21 | syl2imc 41 |
. . . . . . . . . . . . 13
⊢ (𝑃:∅⟶𝑌 → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁))) |
23 | 3, 22 | sylbir 234 |
. . . . . . . . . . . 12
⊢ (𝑃 = ∅ → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁))) |
24 | 23 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁)) |
25 | 2, 24 | syl6bi 252 |
. . . . . . . . . 10
⊢ (𝐹 = 𝑃 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁))) |
26 | 25 | com3l 89 |
. . . . . . . . 9
⊢ ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐹 = 𝑃 → 0 = 𝑁))) |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 = 0 → ((𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐹 = 𝑃 → 0 = 𝑁)))) |
28 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (0..^𝑀) = (0..^0)) |
29 | | fzo0 13392 |
. . . . . . . . . . . 12
⊢ (0..^0) =
∅ |
30 | 28, 29 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → (0..^𝑀) = ∅) |
31 | 30 | feq2d 6582 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:∅⟶𝑋)) |
32 | | f0bi 6653 |
. . . . . . . . . 10
⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅) |
33 | 31, 32 | bitrdi 286 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅)) |
34 | 33 | anbi1d 629 |
. . . . . . . 8
⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌))) |
35 | | eqeq1 2743 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ 0 = 𝑁)) |
36 | 35 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑀 = 0 → ((𝐹 = 𝑃 → 𝑀 = 𝑁) ↔ (𝐹 = 𝑃 → 0 = 𝑁))) |
37 | 36 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑀 = 0 → (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐹 = 𝑃 → 𝑀 = 𝑁)) ↔ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐹 = 𝑃 → 0 = 𝑁)))) |
38 | 27, 34, 37 | 3imtr4d 293 |
. . . . . . 7
⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐹 = 𝑃 → 𝑀 = 𝑁)))) |
39 | 38 | com3l 89 |
. . . . . 6
⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁)))) |
40 | 39 | impcom 407 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝐹 = 𝑃 → 𝑀 = 𝑁))) |
41 | 40 | impcom 407 |
. . . 4
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 → 𝑀 = 𝑁)) |
42 | 28 | feq2d 6582 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:(0..^0)⟶𝑋)) |
43 | 29 | feq2i 6588 |
. . . . . . . . . . . . 13
⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹:∅⟶𝑋) |
44 | 43, 32 | bitri 274 |
. . . . . . . . . . . 12
⊢ (𝐹:(0..^0)⟶𝑋 ↔ 𝐹 = ∅) |
45 | 42, 44 | bitrdi 286 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅)) |
46 | 45 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅)) |
47 | | eqeq1 2743 |
. . . . . . . . . . . 12
⊢ (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0)) |
48 | 47 | biimpac 478 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0) |
49 | | oveq2 7276 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0)) |
50 | 49 | feq2d 6582 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃:(0..^0)⟶𝑌)) |
51 | 29 | feq2i 6588 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃:∅⟶𝑌) |
52 | 51, 3 | bitri 274 |
. . . . . . . . . . . 12
⊢ (𝑃:(0..^0)⟶𝑌 ↔ 𝑃 = ∅) |
53 | 50, 52 | bitrdi 286 |
. . . . . . . . . . 11
⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅)) |
54 | 48, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃 = ∅)) |
55 | 46, 54 | anbi12d 630 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃 = ∅))) |
56 | | eqtr3 2765 |
. . . . . . . . 9
⊢ ((𝐹 = ∅ ∧ 𝑃 = ∅) → 𝐹 = 𝑃) |
57 | 55, 56 | syl6bi 252 |
. . . . . . . 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..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃))) |
61 | 60 | impcom 407 |
. . . 4
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 → 𝐹 = 𝑃)) |
62 | 41, 61 | impbid 211 |
. . 3
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ 𝑀 = 𝑁)) |
63 | | ral0 4448 |
. . . . . 6
⊢
∀𝑖 ∈
∅ (𝐹‘𝑖) = (𝑃‘𝑖) |
64 | 30 | raleqdv 3346 |
. . . . . 6
⊢ (𝑀 = 0 → (∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝐹‘𝑖) = (𝑃‘𝑖))) |
65 | 63, 64 | mpbiri 257 |
. . . . 5
⊢ (𝑀 = 0 → ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) |
66 | 65 | biantrud 531 |
. . . 4
⊢ (𝑀 = 0 → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
67 | 66 | adantr 480 |
. . 3
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
68 | 62, 67 | bitrd 278 |
. 2
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
69 | | ffn 6596 |
. . . . . . 7
⊢ (𝐹:(0..^𝑀)⟶𝑋 → 𝐹 Fn (0..^𝑀)) |
70 | 69, 4 | anim12i 612 |
. . . . . 6
⊢ ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁))) |
71 | 70 | adantl 481 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁))) |
72 | 71 | adantl 481 |
. . . 4
⊢ ((¬
𝑀 = 0 ∧ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁))) |
73 | | eqfnfv2 6904 |
. . . 4
⊢ ((𝐹 Fn (0..^𝑀) ∧ 𝑃 Fn (0..^𝑁)) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
74 | 72, 73 | syl 17 |
. . 3
⊢ ((¬
𝑀 = 0 ∧ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
75 | | df-ne 2945 |
. . . . . 6
⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0) |
76 | | elnnne0 12230 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 𝑀 ≠
0)) |
77 | | 0zd 12314 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 ∈
ℤ) |
78 | | nnz 12325 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
79 | | nngt0 11987 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
80 | 77, 78, 79 | 3jca 1126 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀)) |
82 | | fzoopth 44771 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 0 < 𝑀) → ((0..^𝑀) = (0..^𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((0..^𝑀) =
(0..^𝑁) ↔ (0 = 0 ∧
𝑀 = 𝑁))) |
84 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((0 = 0
∧ 𝑀 = 𝑁) → 𝑀 = 𝑁) |
85 | 83, 84 | syl6bi 252 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((0..^𝑀) =
(0..^𝑁) → 𝑀 = 𝑁)) |
86 | 85 | anim1d 610 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
87 | | oveq2 7276 |
. . . . . . . . . . 11
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
88 | 87 | anim1i 614 |
. . . . . . . . . 10
⊢ ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))) |
89 | 86, 88 | impbid1 224 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
90 | 89 | ex 412 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ0
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
91 | 76, 90 | sylbir 234 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≠ 0) →
(𝑁 ∈
ℕ0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
92 | 91 | impancom 451 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
93 | 75, 92 | syl5bir 242 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
94 | 93 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (¬ 𝑀 = 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
95 | 94 | impcom 407 |
. . 3
⊢ ((¬
𝑀 = 0 ∧ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
96 | 74, 95 | bitrd 278 |
. 2
⊢ ((¬
𝑀 = 0 ∧ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
97 | 68, 96 | pm2.61ian 808 |
1
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |