Proof of Theorem hashimarn
Step | Hyp | Ref
| Expression |
1 | | f1f 6014 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
2 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ran 𝐹 ⊆ dom 𝐸) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ⊆ dom 𝐸) |
4 | 3 | adantl 481 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → ran 𝐹 ⊆ dom 𝐸) |
5 | | ssdmres 5340 |
. . . . 5
⊢ (ran
𝐹 ⊆ dom 𝐸 ↔ dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
6 | 4, 5 | sylib 207 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
7 | 6 | fveq2d 6107 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘dom (𝐸 ↾ ran 𝐹)) = (#‘ran 𝐹)) |
8 | | f1fun 6016 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → Fun 𝐸) |
9 | | funres 5843 |
. . . . . . . . 9
⊢ (Fun
𝐸 → Fun (𝐸 ↾ ran 𝐹)) |
10 | | funfn 5833 |
. . . . . . . . 9
⊢ (Fun
(𝐸 ↾ ran 𝐹) ↔ (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
11 | 9, 10 | sylib 207 |
. . . . . . . 8
⊢ (Fun
𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
12 | 8, 11 | syl 17 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
13 | 12 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
14 | | hashfn 13025 |
. . . . . 6
⊢ ((𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹) → (#‘(𝐸 ↾ ran 𝐹)) = (#‘dom (𝐸 ↾ ran 𝐹))) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘(𝐸 ↾ ran 𝐹)) = (#‘dom (𝐸 ↾ ran 𝐹))) |
16 | | ovex 6577 |
. . . . . . . 8
⊢
(0..^(#‘𝐹))
∈ V |
17 | | fex 6394 |
. . . . . . . 8
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (0..^(#‘𝐹)) ∈ V) → 𝐹 ∈ V) |
18 | 1, 16, 17 | sylancl 693 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → 𝐹 ∈ V) |
19 | | rnexg 6990 |
. . . . . . 7
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ∈ V) |
21 | | simpll 786 |
. . . . . . 7
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
22 | | f1ssres 6021 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ran 𝐹 ⊆ dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
23 | 21, 4, 22 | syl2anc 691 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
24 | | hashf1rn 13004 |
. . . . . 6
⊢ ((ran
𝐹 ∈ V ∧ (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) → (#‘(𝐸 ↾ ran 𝐹)) = (#‘ran (𝐸 ↾ ran 𝐹))) |
25 | 20, 23, 24 | syl2an2 871 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘(𝐸 ↾ ran 𝐹)) = (#‘ran (𝐸 ↾ ran 𝐹))) |
26 | 15, 25 | eqtr3d 2646 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘dom (𝐸 ↾ ran 𝐹)) = (#‘ran (𝐸 ↾ ran 𝐹))) |
27 | | df-ima 5051 |
. . . . 5
⊢ (𝐸 “ ran 𝐹) = ran (𝐸 ↾ ran 𝐹) |
28 | 27 | fveq2i 6106 |
. . . 4
⊢
(#‘(𝐸 “
ran 𝐹)) = (#‘ran
(𝐸 ↾ ran 𝐹)) |
29 | 26, 28 | syl6reqr 2663 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘(𝐸 “ ran 𝐹)) = (#‘dom (𝐸 ↾ ran 𝐹))) |
30 | | hashf1rn 13004 |
. . . . 5
⊢
(((0..^(#‘𝐹))
∈ V ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘𝐹) = (#‘ran 𝐹)) |
31 | 16, 30 | mpan 702 |
. . . 4
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → (#‘𝐹) = (#‘ran 𝐹)) |
32 | 31 | adantl 481 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘𝐹) = (#‘ran 𝐹)) |
33 | 7, 29, 32 | 3eqtr4d 2654 |
. 2
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) → (#‘(𝐸 “ ran 𝐹)) = (#‘𝐹)) |
34 | 33 | ex 449 |
1
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → (#‘(𝐸 “ ran 𝐹)) = (#‘𝐹))) |