Step | Hyp | Ref
| Expression |
1 | | ffn 5347 |
. . . . . 6
⊢ (𝐹:(0...𝐾)⟶𝑉 → 𝐹 Fn (0...𝐾)) |
2 | 1 | adantr 274 |
. . . . 5
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 𝐹 Fn (0...𝐾)) |
3 | | 0nn0 9150 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
4 | 3 | a1i 9 |
. . . . . 6
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 0 ∈
ℕ0) |
5 | | simpr 109 |
. . . . . 6
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℕ0) |
6 | | nn0ge0 9160 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 0 ≤ 𝐾) |
7 | 6 | adantl 275 |
. . . . . 6
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 0 ≤
𝐾) |
8 | | elfz2nn0 10068 |
. . . . . 6
⊢ (0 ∈
(0...𝐾) ↔ (0 ∈
ℕ0 ∧ 𝐾
∈ ℕ0 ∧ 0 ≤ 𝐾)) |
9 | 4, 5, 7, 8 | syl3anbrc 1176 |
. . . . 5
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 0 ∈
(0...𝐾)) |
10 | | id 19 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℕ0) |
11 | | nn0re 9144 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
12 | 11 | leidd 8433 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ≤ 𝐾) |
13 | | elfz2nn0 10068 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝐾) ↔ (𝐾 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0
∧ 𝐾 ≤ 𝐾)) |
14 | 10, 10, 12, 13 | syl3anbrc 1176 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈ (0...𝐾)) |
15 | 14 | adantl 275 |
. . . . 5
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ (0...𝐾)) |
16 | | fnimapr 5556 |
. . . . 5
⊢ ((𝐹 Fn (0...𝐾) ∧ 0 ∈ (0...𝐾) ∧ 𝐾 ∈ (0...𝐾)) → (𝐹 “ {0, 𝐾}) = {(𝐹‘0), (𝐹‘𝐾)}) |
17 | 2, 9, 15, 16 | syl3anc 1233 |
. . . 4
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝐹 “ {0, 𝐾}) = {(𝐹‘0), (𝐹‘𝐾)}) |
18 | 17 | ineq1d 3327 |
. . 3
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → ((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ({(𝐹‘0), (𝐹‘𝐾)} ∩ (𝐹 “ (1..^𝐾)))) |
19 | 18 | eqeq1d 2179 |
. 2
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ({(𝐹‘0), (𝐹‘𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅)) |
20 | | disj 3463 |
. . 3
⊢ (({(𝐹‘0), (𝐹‘𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ∀𝑣 ∈ {(𝐹‘0), (𝐹‘𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾))) |
21 | | simpl 108 |
. . . . 5
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → 𝐹:(0...𝐾)⟶𝑉) |
22 | 21, 9 | ffvelrnd 5632 |
. . . 4
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝐹‘0) ∈ 𝑉) |
23 | 21, 15 | ffvelrnd 5632 |
. . . 4
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (𝐹‘𝐾) ∈ 𝑉) |
24 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑣 = (𝐹‘0) → (𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)))) |
25 | 24 | notbid 662 |
. . . . . 6
⊢ (𝑣 = (𝐹‘0) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)))) |
26 | | df-nel 2436 |
. . . . . 6
⊢ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾))) |
27 | 25, 26 | bitr4di 197 |
. . . . 5
⊢ (𝑣 = (𝐹‘0) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘0) ∉ (𝐹 “ (1..^𝐾)))) |
28 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑣 = (𝐹‘𝐾) → (𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)))) |
29 | 28 | notbid 662 |
. . . . . 6
⊢ (𝑣 = (𝐹‘𝐾) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾)))) |
30 | | df-nel 2436 |
. . . . . 6
⊢ ((𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘𝐾) ∈ (𝐹 “ (1..^𝐾))) |
31 | 29, 30 | bitr4di 197 |
. . . . 5
⊢ (𝑣 = (𝐹‘𝐾) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾)))) |
32 | 27, 31 | ralprg 3634 |
. . . 4
⊢ (((𝐹‘0) ∈ 𝑉 ∧ (𝐹‘𝐾) ∈ 𝑉) → (∀𝑣 ∈ {(𝐹‘0), (𝐹‘𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |
33 | 22, 23, 32 | syl2anc 409 |
. . 3
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) →
(∀𝑣 ∈ {(𝐹‘0), (𝐹‘𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |
34 | 20, 33 | syl5bb 191 |
. 2
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) →
(({(𝐹‘0), (𝐹‘𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |
35 | 19, 34 | bitrd 187 |
1
⊢ ((𝐹:(0...𝐾)⟶𝑉 ∧ 𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹‘𝐾) ∉ (𝐹 “ (1..^𝐾))))) |