Proof of Theorem 2ffzoeq
| Step | Hyp | Ref
| Expression |
| 1 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝐹 = 𝑃 → (𝐹 = ∅ ↔ 𝑃 = ∅)) |
| 2 | 1 | anbi1d 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
→ 𝑁 ∈
ℤ) |
| 9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℤ) |
| 10 | | fzon 13720 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (𝑁
≤ 0 ↔ (0..^𝑁) =
∅)) |
| 11 | 7, 9, 10 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 0 ↔ (0..^𝑁) = ∅)) |
| 12 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
| 13 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ ℝ) |
| 14 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 15 | 13, 14 | letri3d 11403 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (0 = 𝑁 ↔ (0
≤ 𝑁 ∧ 𝑁 ≤ 0))) |
| 16 | 15 | biimprd 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((0 ≤ 𝑁 ∧
𝑁 ≤ 0) → 0 = 𝑁)) |
| 17 | 12, 16 | mpand 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ≤ 0 → 0 =
𝑁)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 0 → 0 = 𝑁)) |
| 19 | 11, 18 | sylbird 260 |
. . . . . . . . . . . . . . . 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 235 |
. . . . . . . . . . . 12
⊢ (𝑃 = ∅ → (𝑃:(0..^𝑁)⟶𝑌 → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁))) |
| 24 | 23 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝑃 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 0 = 𝑁)) |
| 25 | 2, 24 | biimtrdi 253 |
. . . . . . . . . 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 7439 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (0..^𝑀) = (0..^0)) |
| 29 | | fzo0 13723 |
. . . . . . . . . . . 12
⊢ (0..^0) =
∅ |
| 30 | 28, 29 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑀 = 0 → (0..^𝑀) = ∅) |
| 31 | 30 | feq2d 6722 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:∅⟶𝑋)) |
| 32 | | f0bi 6791 |
. . . . . . . . . 10
⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅) |
| 33 | 31, 32 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹 = ∅)) |
| 34 | 33 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑀 = 0 → ((𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌) ↔ (𝐹 = ∅ ∧ 𝑃:(0..^𝑁)⟶𝑌))) |
| 35 | | eqeq1 2741 |
. . . . . . . . . 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 294 |
. . . . . . 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 6722 |
. . . . . . . . . . . 12
⊢ (𝑀 = 0 → (𝐹:(0..^𝑀)⟶𝑋 ↔ 𝐹:(0..^0)⟶𝑋)) |
| 43 | 29 | feq2i 6728 |
. . . . . . . . . . . . 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 2741 |
. . . . . . . . . . . 12
⊢ (𝑀 = 𝑁 → (𝑀 = 0 ↔ 𝑁 = 0)) |
| 48 | 47 | biimpac 478 |
. . . . . . . . . . 11
⊢ ((𝑀 = 0 ∧ 𝑀 = 𝑁) → 𝑁 = 0) |
| 49 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → (0..^𝑁) = (0..^0)) |
| 50 | 49 | feq2d 6722 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑃:(0..^𝑁)⟶𝑌 ↔ 𝑃:(0..^0)⟶𝑌)) |
| 51 | 29 | feq2i 6728 |
. . . . . . . . . . . . 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 2763 |
. . . . . . . . 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..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝑀 = 0 → (𝑀 = 𝑁 → 𝐹 = 𝑃))) |
| 61 | 60 | impcom 407 |
. . . 4
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 → 𝐹 = 𝑃)) |
| 62 | 41, 61 | impbid 212 |
. . 3
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ 𝑀 = 𝑁)) |
| 63 | | ral0 4513 |
. . . . . 6
⊢
∀𝑖 ∈
∅ (𝐹‘𝑖) = (𝑃‘𝑖) |
| 64 | 30 | raleqdv 3326 |
. . . . . 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..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝑀 = 𝑁 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
| 68 | 62, 67 | bitrd 279 |
. 2
⊢ ((𝑀 = 0 ∧ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
| 69 | | ffn 6736 |
. . . . . . 7
⊢ (𝐹:(0..^𝑀)⟶𝑋 → 𝐹 Fn (0..^𝑀)) |
| 70 | 69, 4 | anim12i 613 |
. . . . . 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 7052 |
. . . 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 2941 |
. . . . . 6
⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0) |
| 76 | | elnnne0 12540 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 𝑀 ≠
0)) |
| 77 | | 0zd 12625 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 ∈
ℤ) |
| 78 | | nnz 12634 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 79 | | nngt0 12297 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 0 <
𝑀) |
| 80 | 77, 78, 79 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀)) |
| 82 | | fzoopth 13801 |
. . . . . . . . . . . . 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 | biimtrdi 253 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ ((0..^𝑀) =
(0..^𝑁) → 𝑀 = 𝑁)) |
| 86 | 85 | anim1d 611 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
| 87 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑀 = 𝑁 → (0..^𝑀) = (0..^𝑁)) |
| 88 | 87 | anim1i 615 |
. . . . . . . . . 10
⊢ ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) → ((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))) |
| 89 | 86, 88 | impbid1 225 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
| 90 | 89 | ex 412 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ0
→ (((0..^𝑀) =
(0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
| 91 | 76, 90 | sylbir 235 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≠ 0) →
(𝑁 ∈
ℕ0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
| 92 | 91 | impancom 451 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≠ 0 → (((0..^𝑀) = (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))) |
| 93 | 75, 92 | biimtrrid 243 |
. . . . 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 279 |
. 2
⊢ ((¬
𝑀 = 0 ∧ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌))) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |
| 97 | 68, 96 | pm2.61ian 812 |
1
⊢ (((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) |