Step | Hyp | Ref
| Expression |
1 | | simplr 785 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ 𝑆 ∈ Fin) |
2 | | fzfi 13073 |
. . . 4
⊢
(1...𝑁) ∈
Fin |
3 | | difinf 8505 |
. . . 4
⊢ ((¬
𝑆 ∈ Fin ∧
(1...𝑁) ∈ Fin) →
¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
4 | 1, 2, 3 | sylancl 580 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
5 | | fzfi 13073 |
. . . 4
⊢
(1...𝐴) ∈
Fin |
6 | | diffi 8467 |
. . . 4
⊢
((1...𝐴) ∈ Fin
→ ((1...𝐴) ∖
(1...𝑁)) ∈
Fin) |
7 | 5, 6 | ax-mp 5 |
. . 3
⊢
((1...𝐴) ∖
(1...𝑁)) ∈
Fin |
8 | | isinffi 9138 |
. . 3
⊢ ((¬
(𝑆 ∖ (1...𝑁)) ∈ Fin ∧ ((1...𝐴) ∖ (1...𝑁)) ∈ Fin) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
9 | 4, 7, 8 | sylancl 580 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
10 | | f1f1orn 6393 |
. . . . . . . 8
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1-onto→ran
𝑎) |
11 | 10 | adantl 475 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1-onto→ran
𝑎) |
12 | | f1oi 6419 |
. . . . . . . 8
⊢ ( I
↾ (1...𝑁)):(1...𝑁)–1-1-onto→(1...𝑁) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ( I ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | | incom 4034 |
. . . . . . . . 9
⊢
(((1...𝐴) ∖
(1...𝑁)) ∩ (1...𝑁)) = ((1...𝑁) ∩ ((1...𝐴) ∖ (1...𝑁))) |
15 | | disjdif 4265 |
. . . . . . . . 9
⊢
((1...𝑁) ∩
((1...𝐴) ∖ (1...𝑁))) = ∅ |
16 | 14, 15 | eqtri 2849 |
. . . . . . . 8
⊢
(((1...𝐴) ∖
(1...𝑁)) ∩ (1...𝑁)) = ∅ |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅) |
18 | | f1f 6342 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → 𝑎:((1...𝐴) ∖ (1...𝑁))⟶(𝑆 ∖ (1...𝑁))) |
19 | 18 | frnd 6289 |
. . . . . . . . . . 11
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
20 | 19 | adantl 475 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
21 | 20 | ssrind 4066 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁))) |
22 | | incom 4034 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁)) = ((1...𝑁) ∩ (𝑆 ∖ (1...𝑁))) |
23 | | disjdif 4265 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(𝑆 ∖ (1...𝑁))) = ∅ |
24 | 22, 23 | eqtri 2849 |
. . . . . . . . 9
⊢ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅ |
25 | 21, 24 | syl6sseq 3876 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ∅) |
26 | | ss0 4201 |
. . . . . . . 8
⊢ ((ran
𝑎 ∩ (1...𝑁)) ⊆ ∅ → (ran
𝑎 ∩ (1...𝑁)) = ∅) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) = ∅) |
28 | | f1oun 6401 |
. . . . . . 7
⊢ (((𝑎:((1...𝐴) ∖ (1...𝑁))–1-1-onto→ran
𝑎 ∧ ( I ↾
(1...𝑁)):(1...𝑁)–1-1-onto→(1...𝑁)) ∧ ((((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅ ∧ (ran 𝑎 ∩ (1...𝑁)) = ∅)) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁))) |
29 | 11, 13, 17, 27, 28 | syl22anc 872 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁))) |
30 | | f1of1 6381 |
. . . . . 6
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁)) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
32 | | uncom 3986 |
. . . . . . 7
⊢
(((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) |
33 | | simplrr 796 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → 𝐴 ∈ (ℤ≥‘𝑁)) |
34 | | fzss2 12681 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝐴)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ (1...𝐴)) |
36 | | undif 4274 |
. . . . . . . 8
⊢
((1...𝑁) ⊆
(1...𝐴) ↔ ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
37 | 35, 36 | sylib 210 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
38 | 32, 37 | syl5eq 2873 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁)) = (1...𝐴)) |
39 | | f1eq2 6338 |
. . . . . 6
⊢
((((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = (1...𝐴) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)))) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)))) |
41 | 31, 40 | mpbid 224 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁))) |
42 | 19 | difss2d 3969 |
. . . . . 6
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ 𝑆) |
43 | 42 | adantl 475 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ 𝑆) |
44 | | simplrl 795 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ 𝑆) |
45 | 43, 44 | unssd 4018 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) |
46 | | f1ss 6347 |
. . . 4
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)) ∧ (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
47 | 41, 45, 46 | syl2anc 579 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
48 | | resundir 5652 |
. . . 4
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) |
49 | | dmres 5659 |
. . . . . . . 8
⊢ dom
(𝑎 ↾ (1...𝑁)) = ((1...𝑁) ∩ dom 𝑎) |
50 | | incom 4034 |
. . . . . . . . 9
⊢
((1...𝑁) ∩ dom
𝑎) = (dom 𝑎 ∩ (1...𝑁)) |
51 | | f1dm 6346 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
52 | 51 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
53 | 52 | ineq1d 4042 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁))) |
54 | 53, 16 | syl6eq 2877 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = ∅) |
55 | 50, 54 | syl5eq 2873 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∩ dom 𝑎) = ∅) |
56 | 49, 55 | syl5eq 2873 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom (𝑎 ↾ (1...𝑁)) = ∅) |
57 | | relres 5666 |
. . . . . . . 8
⊢ Rel
(𝑎 ↾ (1...𝑁)) |
58 | | reldm0 5579 |
. . . . . . . 8
⊢ (Rel
(𝑎 ↾ (1...𝑁)) → ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅) |
60 | 56, 59 | sylibr 226 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ↾ (1...𝑁)) = ∅) |
61 | | residm 5670 |
. . . . . . 7
⊢ (( I
↾ (1...𝑁)) ↾
(1...𝑁)) = ( I ↾
(1...𝑁)) |
62 | 61 | a1i 11 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (( I ↾ (1...𝑁)) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
63 | 60, 62 | uneq12d 3997 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = (∅ ∪ ( I ↾ (1...𝑁)))) |
64 | | uncom 3986 |
. . . . . 6
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= (( I ↾ (1...𝑁))
∪ ∅) |
65 | | un0 4194 |
. . . . . 6
⊢ (( I
↾ (1...𝑁)) ∪
∅) = ( I ↾ (1...𝑁)) |
66 | 64, 65 | eqtri 2849 |
. . . . 5
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= ( I ↾ (1...𝑁)) |
67 | 63, 66 | syl6eq 2877 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = ( I ↾ (1...𝑁))) |
68 | 48, 67 | syl5eq 2873 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
69 | | vex 3417 |
. . . . 5
⊢ 𝑎 ∈ V |
70 | | ovex 6942 |
. . . . . 6
⊢
(1...𝑁) ∈
V |
71 | | resiexg 7369 |
. . . . . 6
⊢
((1...𝑁) ∈ V
→ ( I ↾ (1...𝑁))
∈ V) |
72 | 70, 71 | ax-mp 5 |
. . . . 5
⊢ ( I
↾ (1...𝑁)) ∈
V |
73 | 69, 72 | unex 7221 |
. . . 4
⊢ (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V |
74 | | f1eq1 6337 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐:(1...𝐴)–1-1→𝑆 ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆)) |
75 | | reseq1 5627 |
. . . . . 6
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐 ↾ (1...𝑁)) = ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁))) |
76 | 75 | eqeq1d 2827 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
77 | 74, 76 | anbi12d 624 |
. . . 4
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))) |
78 | 73, 77 | spcev 3517 |
. . 3
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
79 | 47, 68, 78 | syl2anc 579 |
. 2
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
80 | 9, 79 | exlimddv 2034 |
1
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |