Proof of Theorem hashimarn
| Step | Hyp | Ref
| Expression |
| 1 | | f1f 6804 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐸) |
| 2 | 1 | frnd 6744 |
. . . . . 6
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ⊆ dom 𝐸) |
| 3 | 2 | adantl 481 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → ran 𝐹 ⊆ dom 𝐸) |
| 4 | | ssdmres 6031 |
. . . . 5
⊢ (ran
𝐹 ⊆ dom 𝐸 ↔ dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
| 5 | 3, 4 | sylib 218 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → dom (𝐸 ↾ ran 𝐹) = ran 𝐹) |
| 6 | 5 | fveq2d 6910 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘dom (𝐸 ↾ ran 𝐹)) = (♯‘ran 𝐹)) |
| 7 | | df-ima 5698 |
. . . . 5
⊢ (𝐸 “ ran 𝐹) = ran (𝐸 ↾ ran 𝐹) |
| 8 | 7 | fveq2i 6909 |
. . . 4
⊢
(♯‘(𝐸
“ ran 𝐹)) =
(♯‘ran (𝐸
↾ ran 𝐹)) |
| 9 | | f1fun 6806 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → Fun 𝐸) |
| 10 | | funres 6608 |
. . . . . . . . 9
⊢ (Fun
𝐸 → Fun (𝐸 ↾ ran 𝐹)) |
| 11 | 10 | funfnd 6597 |
. . . . . . . 8
⊢ (Fun
𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
| 12 | 9, 11 | syl 17 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
| 13 | 12 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹) Fn dom (𝐸 ↾ ran 𝐹)) |
| 14 | | hashfn 14414 |
. . . . . 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 7464 |
. . . . . . . 8
⊢
(0..^(♯‘𝐹)) ∈ V |
| 17 | | fex 7246 |
. . . . . . . 8
⊢ ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐸 ∧ (0..^(♯‘𝐹)) ∈ V) → 𝐹 ∈ V) |
| 18 | 1, 16, 17 | sylancl 586 |
. . . . . . 7
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → 𝐹 ∈ V) |
| 19 | | rnexg 7924 |
. . . . . . 7
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
| 20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → ran 𝐹 ∈ V) |
| 21 | | simpll 767 |
. . . . . . 7
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
| 22 | | f1ssres 6811 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ran 𝐹 ⊆ dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
| 23 | 21, 3, 22 | syl2anc 584 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) |
| 24 | | hashf1rn 14391 |
. . . . . 6
⊢ ((ran
𝐹 ∈ V ∧ (𝐸 ↾ ran 𝐹):ran 𝐹–1-1→ran 𝐸) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
| 25 | 20, 23, 24 | syl2an2 686 |
. . . . 5
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
| 26 | 15, 25 | eqtr3d 2779 |
. . . 4
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘dom (𝐸 ↾ ran 𝐹)) = (♯‘ran (𝐸 ↾ ran 𝐹))) |
| 27 | 8, 26 | eqtr4id 2796 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 “ ran 𝐹)) = (♯‘dom (𝐸 ↾ ran 𝐹))) |
| 28 | | hashf1rn 14391 |
. . . . 5
⊢
(((0..^(♯‘𝐹)) ∈ V ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘𝐹) = (♯‘ran 𝐹)) |
| 29 | 16, 28 | mpan 690 |
. . . 4
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → (♯‘𝐹) = (♯‘ran 𝐹)) |
| 30 | 29 | adantl 481 |
. . 3
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘𝐹) = (♯‘ran 𝐹)) |
| 31 | 6, 27, 30 | 3eqtr4d 2787 |
. 2
⊢ (((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) ∧ 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸) → (♯‘(𝐸 “ ran 𝐹)) = (♯‘𝐹)) |
| 32 | 31 | ex 412 |
1
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐸 → (♯‘(𝐸 “ ran 𝐹)) = (♯‘𝐹))) |