MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  injresinjlem Structured version   Visualization version   GIF version

Theorem injresinjlem 12571
Description: Lemma for injresinj 12572. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Proof shortened by AV, 14-Feb-2021.) (Revised by Thierry Arnoux, 23-Dec-2021.)
Assertion
Ref Expression
injresinjlem 𝑌 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑋 ∈ (0...𝐾) ∧ 𝑌 ∈ (0...𝐾)) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))

Proof of Theorem injresinjlem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elfznelfzo 12557 . . . . . . 7 ((𝑌 ∈ (0...𝐾) ∧ ¬ 𝑌 ∈ (1..^𝐾)) → (𝑌 = 0 ∨ 𝑌 = 𝐾))
2 fvinim0ffz 12570 . . . . . . . . . . . . 13 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))
3 df-nel 2895 . . . . . . . . . . . . . . . . . 18 ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)))
4 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . 23 (0 = 𝑌 → (𝐹‘0) = (𝐹𝑌))
54eqcoms 2628 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = 0 → (𝐹‘0) = (𝐹𝑌))
65eleq1d 2684 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 0 → ((𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
76notbid 308 . . . . . . . . . . . . . . . . . . . 20 (𝑌 = 0 → (¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
87biimpd 219 . . . . . . . . . . . . . . . . . . 19 (𝑌 = 0 → (¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) → ¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
9 ffn 6032 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(0...𝐾)⟶𝑉𝐹 Fn (0...𝐾))
10 1eluzge0 11717 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ (ℤ‘0)
11 fzoss1 12479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (ℤ‘0) → (1..^𝐾) ⊆ (0..^𝐾))
1210, 11mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐾 ∈ ℕ0 → (1..^𝐾) ⊆ (0..^𝐾))
13 fzossfz 12472 . . . . . . . . . . . . . . . . . . . . . . . 24 (0..^𝐾) ⊆ (0...𝐾)
1412, 13syl6ss 3607 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐾 ∈ ℕ0 → (1..^𝐾) ⊆ (0...𝐾))
15 fvelimab 6240 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn (0...𝐾) ∧ (1..^𝐾) ⊆ (0...𝐾)) → ((𝐹𝑌) ∈ (𝐹 “ (1..^𝐾)) ↔ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌)))
169, 14, 15syl2an 494 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → ((𝐹𝑌) ∈ (𝐹 “ (1..^𝐾)) ↔ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌)))
1716notbid 308 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌)))
18 ralnex 2989 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ (1..^𝐾) ¬ (𝐹𝑧) = (𝐹𝑌) ↔ ¬ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌))
19 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑋 → (𝐹𝑧) = (𝐹𝑋))
2019eqeq1d 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑋 → ((𝐹𝑧) = (𝐹𝑌) ↔ (𝐹𝑋) = (𝐹𝑌)))
2120notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑋 → (¬ (𝐹𝑧) = (𝐹𝑌) ↔ ¬ (𝐹𝑋) = (𝐹𝑌)))
2221rspcva 3302 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑋 ∈ (1..^𝐾) ∧ ∀𝑧 ∈ (1..^𝐾) ¬ (𝐹𝑧) = (𝐹𝑌)) → ¬ (𝐹𝑋) = (𝐹𝑌))
23 pm2.21 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (¬ (𝐹𝑋) = (𝐹𝑌) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))
2423a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (𝐹𝑋) = (𝐹𝑌) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))
25242a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ (𝐹𝑋) = (𝐹𝑌) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
2622, 25syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋 ∈ (1..^𝐾) ∧ ∀𝑧 ∈ (1..^𝐾) ¬ (𝐹𝑧) = (𝐹𝑌)) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
2726expcom 451 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑧 ∈ (1..^𝐾) ¬ (𝐹𝑧) = (𝐹𝑌) → (𝑋 ∈ (1..^𝐾) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
2827com24 95 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ (1..^𝐾) ¬ (𝐹𝑧) = (𝐹𝑌) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
2918, 28sylbir 225 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
3029com12 32 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (¬ ∃𝑧 ∈ (1..^𝐾)(𝐹𝑧) = (𝐹𝑌) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
3117, 30sylbid 230 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾)) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
3231com12 32 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾)) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
338, 32syl6com 37 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)) → (𝑌 = 0 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
343, 33sylbi 207 . . . . . . . . . . . . . . . . 17 ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) → (𝑌 = 0 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
3534adantr 481 . . . . . . . . . . . . . . . 16 (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → (𝑌 = 0 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
3635com12 32 . . . . . . . . . . . . . . 15 (𝑌 = 0 → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
37 df-nel 2895 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)))
38 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐾 = 𝑌 → (𝐹𝐾) = (𝐹𝑌))
3938eqcoms 2628 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = 𝐾 → (𝐹𝐾) = (𝐹𝑌))
4039eleq1d 2684 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 𝐾 → ((𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
4140notbid 308 . . . . . . . . . . . . . . . . . . . 20 (𝑌 = 𝐾 → (¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
4241biimpd 219 . . . . . . . . . . . . . . . . . . 19 (𝑌 = 𝐾 → (¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)) → ¬ (𝐹𝑌) ∈ (𝐹 “ (1..^𝐾))))
4342, 32syl6com 37 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)) → (𝑌 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
4437, 43sylbi 207 . . . . . . . . . . . . . . . . 17 ((𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)) → (𝑌 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
4544adantl 482 . . . . . . . . . . . . . . . 16 (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → (𝑌 = 𝐾 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
4645com12 32 . . . . . . . . . . . . . . 15 (𝑌 = 𝐾 → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
4736, 46jaoi 394 . . . . . . . . . . . . . 14 ((𝑌 = 0 ∨ 𝑌 = 𝐾) → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
4847com13 88 . . . . . . . . . . . . 13 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
492, 48sylbid 230 . . . . . . . . . . . 12 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → (𝑋 ∈ (0...𝐾) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
5049com14 96 . . . . . . . . . . 11 (𝑋 ∈ (0...𝐾) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
5150com12 32 . . . . . . . . . 10 (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → (𝑋 ∈ (0...𝐾) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝑋 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
5251com15 101 . . . . . . . . 9 (𝑋 ∈ (1..^𝐾) → (𝑋 ∈ (0...𝐾) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
53 elfznelfzo 12557 . . . . . . . . . . 11 ((𝑋 ∈ (0...𝐾) ∧ ¬ 𝑋 ∈ (1..^𝐾)) → (𝑋 = 0 ∨ 𝑋 = 𝐾))
54 eqtr3 2641 . . . . . . . . . . . . . 14 ((𝑋 = 0 ∧ 𝑌 = 0) → 𝑋 = 𝑌)
55 2a1 28 . . . . . . . . . . . . . . 15 (𝑋 = 𝑌 → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))
56552a1d 26 . . . . . . . . . . . . . 14 (𝑋 = 𝑌 → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
5754, 56syl 17 . . . . . . . . . . . . 13 ((𝑋 = 0 ∧ 𝑌 = 0) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
585adantl 482 . . . . . . . . . . . . . . . 16 ((𝑋 = 𝐾𝑌 = 0) → (𝐹‘0) = (𝐹𝑌))
59 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝐾 = 𝑋 → (𝐹𝐾) = (𝐹𝑋))
6059eqcoms 2628 . . . . . . . . . . . . . . . . 17 (𝑋 = 𝐾 → (𝐹𝐾) = (𝐹𝑋))
6160adantr 481 . . . . . . . . . . . . . . . 16 ((𝑋 = 𝐾𝑌 = 0) → (𝐹𝐾) = (𝐹𝑋))
6258, 61neeq12d 2852 . . . . . . . . . . . . . . 15 ((𝑋 = 𝐾𝑌 = 0) → ((𝐹‘0) ≠ (𝐹𝐾) ↔ (𝐹𝑌) ≠ (𝐹𝑋)))
63 df-ne 2792 . . . . . . . . . . . . . . . 16 ((𝐹𝑌) ≠ (𝐹𝑋) ↔ ¬ (𝐹𝑌) = (𝐹𝑋))
64 pm2.24 121 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑌) = (𝐹𝑋) → (¬ (𝐹𝑌) = (𝐹𝑋) → 𝑋 = 𝑌))
6564eqcoms 2628 . . . . . . . . . . . . . . . . 17 ((𝐹𝑋) = (𝐹𝑌) → (¬ (𝐹𝑌) = (𝐹𝑋) → 𝑋 = 𝑌))
6665com12 32 . . . . . . . . . . . . . . . 16 (¬ (𝐹𝑌) = (𝐹𝑋) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))
6763, 66sylbi 207 . . . . . . . . . . . . . . 15 ((𝐹𝑌) ≠ (𝐹𝑋) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))
6862, 67syl6bi 243 . . . . . . . . . . . . . 14 ((𝑋 = 𝐾𝑌 = 0) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))
69682a1d 26 . . . . . . . . . . . . 13 ((𝑋 = 𝐾𝑌 = 0) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
70 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (0 = 𝑋 → (𝐹‘0) = (𝐹𝑋))
7170eqcoms 2628 . . . . . . . . . . . . . . . . 17 (𝑋 = 0 → (𝐹‘0) = (𝐹𝑋))
7271adantr 481 . . . . . . . . . . . . . . . 16 ((𝑋 = 0 ∧ 𝑌 = 𝐾) → (𝐹‘0) = (𝐹𝑋))
7339adantl 482 . . . . . . . . . . . . . . . 16 ((𝑋 = 0 ∧ 𝑌 = 𝐾) → (𝐹𝐾) = (𝐹𝑌))
7472, 73neeq12d 2852 . . . . . . . . . . . . . . 15 ((𝑋 = 0 ∧ 𝑌 = 𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) ↔ (𝐹𝑋) ≠ (𝐹𝑌)))
75 df-ne 2792 . . . . . . . . . . . . . . . 16 ((𝐹𝑋) ≠ (𝐹𝑌) ↔ ¬ (𝐹𝑋) = (𝐹𝑌))
7675, 23sylbi 207 . . . . . . . . . . . . . . 15 ((𝐹𝑋) ≠ (𝐹𝑌) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))
7774, 76syl6bi 243 . . . . . . . . . . . . . 14 ((𝑋 = 0 ∧ 𝑌 = 𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))
78772a1d 26 . . . . . . . . . . . . 13 ((𝑋 = 0 ∧ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
79 eqtr3 2641 . . . . . . . . . . . . . 14 ((𝑋 = 𝐾𝑌 = 𝐾) → 𝑋 = 𝑌)
8079, 56syl 17 . . . . . . . . . . . . 13 ((𝑋 = 𝐾𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
8157, 69, 78, 80ccase 986 . . . . . . . . . . . 12 (((𝑋 = 0 ∨ 𝑋 = 𝐾) ∧ (𝑌 = 0 ∨ 𝑌 = 𝐾)) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))
8281ex 450 . . . . . . . . . . 11 ((𝑋 = 0 ∨ 𝑋 = 𝐾) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
8353, 82syl 17 . . . . . . . . . 10 ((𝑋 ∈ (0...𝐾) ∧ ¬ 𝑋 ∈ (1..^𝐾)) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
8483expcom 451 . . . . . . . . 9 𝑋 ∈ (1..^𝐾) → (𝑋 ∈ (0...𝐾) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
8552, 84pm2.61i 176 . . . . . . . 8 (𝑋 ∈ (0...𝐾) → ((𝑌 = 0 ∨ 𝑌 = 𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
8685com12 32 . . . . . . 7 ((𝑌 = 0 ∨ 𝑌 = 𝐾) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
871, 86syl 17 . . . . . 6 ((𝑌 ∈ (0...𝐾) ∧ ¬ 𝑌 ∈ (1..^𝐾)) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
8887ex 450 . . . . 5 (𝑌 ∈ (0...𝐾) → (¬ 𝑌 ∈ (1..^𝐾) → (𝑋 ∈ (0...𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
8988com23 86 . . . 4 (𝑌 ∈ (0...𝐾) → (𝑋 ∈ (0...𝐾) → (¬ 𝑌 ∈ (1..^𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌)))))))
9089impcom 446 . . 3 ((𝑋 ∈ (0...𝐾) ∧ 𝑌 ∈ (0...𝐾)) → (¬ 𝑌 ∈ (1..^𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
9190com12 32 . 2 𝑌 ∈ (1..^𝐾) → ((𝑋 ∈ (0...𝐾) ∧ 𝑌 ∈ (0...𝐾)) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
9291com25 99 1 𝑌 ∈ (1..^𝐾) → ((𝐹‘0) ≠ (𝐹𝐾) → ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ → ((𝑋 ∈ (0...𝐾) ∧ 𝑌 ∈ (0...𝐾)) → ((𝐹𝑋) = (𝐹𝑌) → 𝑋 = 𝑌))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wcel 1988  wne 2791  wnel 2894  wral 2909  wrex 2910  cin 3566  wss 3567  c0 3907  {cpr 4170  cima 5107   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  0cc0 9921  1c1 9922  0cn0 11277  cuz 11672  ...cfz 12311  ..^cfzo 12449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-fzo 12450
This theorem is referenced by:  injresinj  12572
  Copyright terms: Public domain W3C validator