Proof of Theorem hashimarn
Step | Hyp | Ref
| Expression |
1 | | f1f 6316 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐸) |
2 | 1 | frnd 6263 |
. . . . . 6
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ⊆ dom 𝐸) |
3 | 2 | adantl 474 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → ran 𝐹 ⊆ dom 𝐸) |
4 | | ssdmres 5630 |
. . . . 5
⊢ (ran
𝐹 ⊆ dom 𝐸 ↔ dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
5 | 3, 4 | sylib 210 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
6 | 5 | fveq2d 6415 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘dom (𝐸 ↾ ran 𝐹)) = (♯‘ran 𝐹)) |
7 | | f1fun 6318 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → Fun 𝐸) |
8 | | funres 6143 |
. . . . . . . . 9
⊢ (Fun
𝐸 → Fun (𝐸 ↾ ran 𝐹)) |
9 | | funfn 6131 |
. . . . . . . . 9
⊢ (Fun
(𝐸 ↾ ran 𝐹) ↔ (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
10 | 8, 9 | sylib 210 |
. . . . . . . 8
⊢ (Fun
𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
11 | 7, 10 | syl 17 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
12 | 11 | ad2antrr 718 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
13 | | hashfn 13414 |
. . . . . 6
⊢ ((𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘dom (𝐸 ↾ ran 𝐹))) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘dom (𝐸 ↾ ran 𝐹))) |
15 | | ovex 6910 |
. . . . . . . 8
⊢
(0..^(♯‘𝐹)) ∈ V |
16 | | fex 6718 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (0..^(♯‘𝐹)) ∈ V) → 𝐹 ∈ V) |
17 | 1, 15, 16 | sylancl 581 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → 𝐹 ∈ V) |
18 | | rnexg 7332 |
. . . . . . 7
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ∈ V) |
20 | | simpll 784 |
. . . . . . 7
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
21 | | f1ssres 6323 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ran 𝐹 ⊆ dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
22 | 20, 3, 21 | syl2anc 580 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
23 | | hashf1rn 13393 |
. . . . . 6
⊢ ((ran
𝐹 ∈ V ∧ (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
24 | 19, 22, 23 | syl2an2 678 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
25 | 14, 24 | eqtr3d 2835 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘dom (𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
26 | | df-ima 5325 |
. . . . 5
⊢ (𝐸 “ ran 𝐹) = ran (𝐸 ↾ ran 𝐹) |
27 | 26 | fveq2i 6414 |
. . . 4
⊢
(♯‘(𝐸
“ ran 𝐹)) =
(♯‘ran (𝐸
↾ ran 𝐹)) |
28 | 25, 27 | syl6reqr 2852 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 “ ran 𝐹)) = (♯‘dom (𝐸 ↾ ran 𝐹))) |
29 | | hashf1rn 13393 |
. . . . 5
⊢
(((0..^(♯‘𝐹)) ∈ V ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘𝐹) = (♯‘ran 𝐹)) |
30 | 15, 29 | mpan 682 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → (♯‘𝐹) = (♯‘ran 𝐹)) |
31 | 30 | adantl 474 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘𝐹) = (♯‘ran 𝐹)) |
32 | 6, 28, 31 | 3eqtr4d 2843 |
. 2
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 “ ran 𝐹)) = (♯‘𝐹)) |
33 | 32 | ex 402 |
1
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → (♯‘(𝐸 “ ran 𝐹)) = (♯‘𝐹))) |