Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ 𝑆 ∈ Fin) |
2 | | fzfi 12633 |
. . . 4
⊢
(1...𝑁) ∈
Fin |
3 | | difinf 8115 |
. . . 4
⊢ ((¬
𝑆 ∈ Fin ∧
(1...𝑁) ∈ Fin) →
¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
4 | 1, 2, 3 | sylancl 693 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
5 | | fzfi 12633 |
. . . 4
⊢
(1...𝐴) ∈
Fin |
6 | | diffi 8077 |
. . . 4
⊢
((1...𝐴) ∈ Fin
→ ((1...𝐴) ∖
(1...𝑁)) ∈
Fin) |
7 | 5, 6 | ax-mp 5 |
. . 3
⊢
((1...𝐴) ∖
(1...𝑁)) ∈
Fin |
8 | | isinffi 8701 |
. . 3
⊢ ((¬
(𝑆 ∖ (1...𝑁)) ∈ Fin ∧ ((1...𝐴) ∖ (1...𝑁)) ∈ Fin) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
9 | 4, 7, 8 | sylancl 693 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
10 | | f1f1orn 6061 |
. . . . . . . 8
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1-onto→ran
𝑎) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1-onto→ran
𝑎) |
12 | | f1oi 6086 |
. . . . . . . 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 3767 |
. . . . . . . . 9
⊢
(((1...𝐴) ∖
(1...𝑁)) ∩ (1...𝑁)) = ((1...𝑁) ∩ ((1...𝐴) ∖ (1...𝑁))) |
15 | | disjdif 3992 |
. . . . . . . . 9
⊢
((1...𝑁) ∩
((1...𝐴) ∖ (1...𝑁))) = ∅ |
16 | 14, 15 | eqtri 2632 |
. . . . . . . 8
⊢
(((1...𝐴) ∖
(1...𝑁)) ∩ (1...𝑁)) = ∅ |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅) |
18 | | f1f 6014 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → 𝑎:((1...𝐴) ∖ (1...𝑁))⟶(𝑆 ∖ (1...𝑁))) |
19 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))⟶(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
21 | 20 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
22 | | ssrin 3800 |
. . . . . . . . . 10
⊢ (ran
𝑎 ⊆ (𝑆 ∖ (1...𝑁)) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁))) |
24 | | incom 3767 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁)) = ((1...𝑁) ∩ (𝑆 ∖ (1...𝑁))) |
25 | | disjdif 3992 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(𝑆 ∖ (1...𝑁))) = ∅ |
26 | 24, 25 | eqtri 2632 |
. . . . . . . . 9
⊢ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅ |
27 | 23, 26 | syl6sseq 3614 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ∅) |
28 | | ss0 3926 |
. . . . . . . 8
⊢ ((ran
𝑎 ∩ (1...𝑁)) ⊆ ∅ → (ran
𝑎 ∩ (1...𝑁)) = ∅) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) = ∅) |
30 | | f1oun 6069 |
. . . . . . 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...𝑁))) |
31 | 11, 13, 17, 29, 30 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁))) |
32 | | f1of1 6049 |
. . . . . 6
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁)) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
34 | | uncom 3719 |
. . . . . . 7
⊢
(((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) |
35 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → 𝐴 ∈ (ℤ≥‘𝑁)) |
36 | | fzss2 12252 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝐴)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ (1...𝐴)) |
38 | | undif 4001 |
. . . . . . . 8
⊢
((1...𝑁) ⊆
(1...𝐴) ↔ ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
39 | 37, 38 | sylib 207 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
40 | 34, 39 | syl5eq 2656 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁)) = (1...𝐴)) |
41 | | f1eq2 6010 |
. . . . . 6
⊢
((((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = (1...𝐴) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)))) |
42 | 40, 41 | 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...𝑁)))) |
43 | 33, 42 | mpbid 221 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁))) |
44 | 20 | difss2d 3702 |
. . . . . 6
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ 𝑆) |
45 | 44 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ 𝑆) |
46 | | simplrl 796 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ 𝑆) |
47 | 45, 46 | unssd 3751 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) |
48 | | f1ss 6019 |
. . . 4
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)) ∧ (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
49 | 43, 47, 48 | syl2anc 691 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
50 | | resundir 5331 |
. . . 4
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) |
51 | | dmres 5339 |
. . . . . . . 8
⊢ dom
(𝑎 ↾ (1...𝑁)) = ((1...𝑁) ∩ dom 𝑎) |
52 | | incom 3767 |
. . . . . . . . 9
⊢
((1...𝑁) ∩ dom
𝑎) = (dom 𝑎 ∩ (1...𝑁)) |
53 | | f1dm 6018 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
54 | 53 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
55 | 54 | ineq1d 3775 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁))) |
56 | 55, 16 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = ∅) |
57 | 52, 56 | syl5eq 2656 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∩ dom 𝑎) = ∅) |
58 | 51, 57 | syl5eq 2656 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom (𝑎 ↾ (1...𝑁)) = ∅) |
59 | | relres 5346 |
. . . . . . . 8
⊢ Rel
(𝑎 ↾ (1...𝑁)) |
60 | | reldm0 5264 |
. . . . . . . 8
⊢ (Rel
(𝑎 ↾ (1...𝑁)) → ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅)) |
61 | 59, 60 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅) |
62 | 58, 61 | sylibr 223 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ↾ (1...𝑁)) = ∅) |
63 | | residm 5350 |
. . . . . . 7
⊢ (( I
↾ (1...𝑁)) ↾
(1...𝑁)) = ( I ↾
(1...𝑁)) |
64 | 63 | a1i 11 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (( I ↾ (1...𝑁)) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
65 | 62, 64 | uneq12d 3730 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = (∅ ∪ ( I ↾ (1...𝑁)))) |
66 | | uncom 3719 |
. . . . . 6
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= (( I ↾ (1...𝑁))
∪ ∅) |
67 | | un0 3919 |
. . . . . 6
⊢ (( I
↾ (1...𝑁)) ∪
∅) = ( I ↾ (1...𝑁)) |
68 | 66, 67 | eqtri 2632 |
. . . . 5
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= ( I ↾ (1...𝑁)) |
69 | 65, 68 | syl6eq 2660 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = ( I ↾ (1...𝑁))) |
70 | 50, 69 | syl5eq 2656 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
71 | | vex 3176 |
. . . . 5
⊢ 𝑎 ∈ V |
72 | | ovex 6577 |
. . . . . 6
⊢
(1...𝑁) ∈
V |
73 | | resiexg 6994 |
. . . . . 6
⊢
((1...𝑁) ∈ V
→ ( I ↾ (1...𝑁))
∈ V) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
⊢ ( I
↾ (1...𝑁)) ∈
V |
75 | 71, 74 | unex 6854 |
. . . 4
⊢ (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V |
76 | | f1eq1 6009 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐:(1...𝐴)–1-1→𝑆 ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆)) |
77 | | reseq1 5311 |
. . . . . 6
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐 ↾ (1...𝑁)) = ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁))) |
78 | 77 | eqeq1d 2612 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
79 | 76, 78 | anbi12d 743 |
. . . 4
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))) |
80 | 75, 79 | spcev 3273 |
. . 3
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
81 | 49, 70, 80 | syl2anc 691 |
. 2
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
82 | 9, 81 | exlimddv 1850 |
1
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |