| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ 𝑆 ∈ Fin) |
| 2 | | fzfi 14013 |
. . . 4
⊢
(1...𝑁) ∈
Fin |
| 3 | | difinf 9349 |
. . . 4
⊢ ((¬
𝑆 ∈ Fin ∧
(1...𝑁) ∈ Fin) →
¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
| 4 | 1, 2, 3 | sylancl 586 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ¬ (𝑆 ∖ (1...𝑁)) ∈ Fin) |
| 5 | | fzfi 14013 |
. . . 4
⊢
(1...𝐴) ∈
Fin |
| 6 | | diffi 9215 |
. . . 4
⊢
((1...𝐴) ∈ Fin
→ ((1...𝐴) ∖
(1...𝑁)) ∈
Fin) |
| 7 | 5, 6 | ax-mp 5 |
. . 3
⊢
((1...𝐴) ∖
(1...𝑁)) ∈
Fin |
| 8 | | isinffi 10032 |
. . 3
⊢ ((¬
(𝑆 ∖ (1...𝑁)) ∈ Fin ∧ ((1...𝐴) ∖ (1...𝑁)) ∈ Fin) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
| 9 | 4, 7, 8 | sylancl 586 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑎 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) |
| 10 | | f1f1orn 6859 |
. . . . . . . 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 6886 |
. . . . . . . 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 | | disjdifr 4473 |
. . . . . . . 8
⊢
(((1...𝐴) ∖
(1...𝑁)) ∩ (1...𝑁)) = ∅ |
| 15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅) |
| 16 | | f1f 6804 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → 𝑎:((1...𝐴) ∖ (1...𝑁))⟶(𝑆 ∖ (1...𝑁))) |
| 17 | 16 | frnd 6744 |
. . . . . . . . . . 11
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
| 18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ (𝑆 ∖ (1...𝑁))) |
| 19 | 18 | ssrind 4244 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁))) |
| 20 | | disjdifr 4473 |
. . . . . . . . 9
⊢ ((𝑆 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅ |
| 21 | 19, 20 | sseqtrdi 4024 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) ⊆ ∅) |
| 22 | | ss0 4402 |
. . . . . . . 8
⊢ ((ran
𝑎 ∩ (1...𝑁)) ⊆ ∅ → (ran
𝑎 ∩ (1...𝑁)) = ∅) |
| 23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∩ (1...𝑁)) = ∅) |
| 24 | | f1oun 6867 |
. . . . . . 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...𝑁))) |
| 25 | 11, 13, 15, 23, 24 | syl22anc 839 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁))) |
| 26 | | f1of1 6847 |
. . . . . 6
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1-onto→(ran
𝑎 ∪ (1...𝑁)) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁))) |
| 28 | | uncom 4158 |
. . . . . . 7
⊢
(((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) |
| 29 | | simplrr 778 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → 𝐴 ∈ (ℤ≥‘𝑁)) |
| 30 | | fzss2 13604 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝐴)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ (1...𝐴)) |
| 32 | | undif 4482 |
. . . . . . . 8
⊢
((1...𝑁) ⊆
(1...𝐴) ↔ ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
| 33 | 31, 32 | sylib 218 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∪ ((1...𝐴) ∖ (1...𝑁))) = (1...𝐴)) |
| 34 | 28, 33 | eqtrid 2789 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁)) = (1...𝐴)) |
| 35 | | f1eq2 6800 |
. . . . . 6
⊢
((((1...𝐴) ∖
(1...𝑁)) ∪ (1...𝑁)) = (1...𝐴) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((1...𝐴) ∖ (1...𝑁)) ∪ (1...𝑁))–1-1→(ran 𝑎 ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)))) |
| 36 | 34, 35 | 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...𝑁)))) |
| 37 | 27, 36 | mpbid 232 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁))) |
| 38 | 17 | difss2d 4139 |
. . . . . 6
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → ran 𝑎 ⊆ 𝑆) |
| 39 | 38 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ran 𝑎 ⊆ 𝑆) |
| 40 | | simplrl 777 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (1...𝑁) ⊆ 𝑆) |
| 41 | 39, 40 | unssd 4192 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) |
| 42 | | f1ss 6809 |
. . . 4
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→(ran 𝑎 ∪ (1...𝑁)) ∧ (ran 𝑎 ∪ (1...𝑁)) ⊆ 𝑆) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
| 43 | 37, 41, 42 | syl2anc 584 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆) |
| 44 | | resundir 6012 |
. . . 4
⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) |
| 45 | | dmres 6030 |
. . . . . . . 8
⊢ dom
(𝑎 ↾ (1...𝑁)) = ((1...𝑁) ∩ dom 𝑎) |
| 46 | | incom 4209 |
. . . . . . . . 9
⊢
((1...𝑁) ∩ dom
𝑎) = (dom 𝑎 ∩ (1...𝑁)) |
| 47 | | f1dm 6808 |
. . . . . . . . . . . 12
⊢ (𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁)) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom 𝑎 = ((1...𝐴) ∖ (1...𝑁))) |
| 49 | 48 | ineq1d 4219 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = (((1...𝐴) ∖ (1...𝑁)) ∩ (1...𝑁))) |
| 50 | 49, 14 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (dom 𝑎 ∩ (1...𝑁)) = ∅) |
| 51 | 46, 50 | eqtrid 2789 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((1...𝑁) ∩ dom 𝑎) = ∅) |
| 52 | 45, 51 | eqtrid 2789 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → dom (𝑎 ↾ (1...𝑁)) = ∅) |
| 53 | | relres 6023 |
. . . . . . . 8
⊢ Rel
(𝑎 ↾ (1...𝑁)) |
| 54 | | reldm0 5938 |
. . . . . . . 8
⊢ (Rel
(𝑎 ↾ (1...𝑁)) → ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅)) |
| 55 | 53, 54 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅) |
| 56 | 52, 55 | sylibr 234 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (𝑎 ↾ (1...𝑁)) = ∅) |
| 57 | | residm 6028 |
. . . . . . 7
⊢ (( I
↾ (1...𝑁)) ↾
(1...𝑁)) = ( I ↾
(1...𝑁)) |
| 58 | 57 | a1i 11 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → (( I ↾ (1...𝑁)) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
| 59 | 56, 58 | uneq12d 4169 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = (∅ ∪ ( I ↾ (1...𝑁)))) |
| 60 | | uncom 4158 |
. . . . . 6
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= (( I ↾ (1...𝑁))
∪ ∅) |
| 61 | | un0 4394 |
. . . . . 6
⊢ (( I
↾ (1...𝑁)) ∪
∅) = ( I ↾ (1...𝑁)) |
| 62 | 60, 61 | eqtri 2765 |
. . . . 5
⊢ (∅
∪ ( I ↾ (1...𝑁)))
= ( I ↾ (1...𝑁)) |
| 63 | 59, 62 | eqtrdi 2793 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = ( I ↾ (1...𝑁))) |
| 64 | 44, 63 | eqtrid 2789 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) |
| 65 | | vex 3484 |
. . . . 5
⊢ 𝑎 ∈ V |
| 66 | | ovex 7464 |
. . . . . 6
⊢
(1...𝑁) ∈
V |
| 67 | | resiexg 7934 |
. . . . . 6
⊢
((1...𝑁) ∈ V
→ ( I ↾ (1...𝑁))
∈ V) |
| 68 | 66, 67 | ax-mp 5 |
. . . . 5
⊢ ( I
↾ (1...𝑁)) ∈
V |
| 69 | 65, 68 | unex 7764 |
. . . 4
⊢ (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V |
| 70 | | f1eq1 6799 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐:(1...𝐴)–1-1→𝑆 ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆)) |
| 71 | | reseq1 5991 |
. . . . . 6
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑐 ↾ (1...𝑁)) = ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁))) |
| 72 | 71 | eqeq1d 2739 |
. . . . 5
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
| 73 | 70, 72 | anbi12d 632 |
. . . 4
⊢ (𝑐 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))) |
| 74 | 69, 73 | spcev 3606 |
. . 3
⊢ (((𝑎 ∪ ( I ↾ (1...𝑁))):(1...𝐴)–1-1→𝑆 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
| 75 | 43, 64, 74 | syl2anc 584 |
. 2
⊢ ((((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) ∧ 𝑎:((1...𝐴) ∖ (1...𝑁))–1-1→(𝑆 ∖ (1...𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |
| 76 | 9, 75 | exlimddv 1935 |
1
⊢ (((𝑁 ∈ ℕ0
∧ ¬ 𝑆 ∈ Fin)
∧ ((1...𝑁) ⊆
𝑆 ∧ 𝐴 ∈ (ℤ≥‘𝑁))) → ∃𝑐(𝑐:(1...𝐴)–1-1→𝑆 ∧ (𝑐 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) |