Proof of Theorem fundcmpsurinjimaid
Step | Hyp | Ref
| Expression |
1 | | fimadmfo 6601 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴)) |
2 | | fundcmpsurinjimaid.g |
. . . . 5
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) |
3 | | ffn 6504 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
4 | | dffn5 6728 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
5 | 3, 4 | sylib 221 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
6 | 5 | eqcomd 2744 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = 𝐹) |
7 | 2, 6 | syl5eq 2785 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐺 = 𝐹) |
8 | | eqidd 2739 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = 𝐴) |
9 | | fundcmpsurinjimaid.i |
. . . . 5
⊢ 𝐼 = (𝐹 “ 𝐴) |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐼 = (𝐹 “ 𝐴)) |
11 | 7, 8, 10 | foeq123d 6611 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐺:𝐴–onto→𝐼 ↔ 𝐹:𝐴–onto→(𝐹 “ 𝐴))) |
12 | 1, 11 | mpbird 260 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → 𝐺:𝐴–onto→𝐼) |
13 | | f1oi 6655 |
. . 3
⊢ ( I
↾ 𝐼):𝐼–1-1-onto→𝐼 |
14 | | f1of1 6617 |
. . 3
⊢ (( I
↾ 𝐼):𝐼–1-1-onto→𝐼 → ( I ↾ 𝐼):𝐼–1-1→𝐼) |
15 | | fundcmpsurinjimaid.h |
. . . . . . 7
⊢ 𝐻 = ( I ↾ 𝐼) |
16 | | f1eq1 6569 |
. . . . . . 7
⊢ (𝐻 = ( I ↾ 𝐼) → (𝐻:𝐼–1-1→𝐼 ↔ ( I ↾ 𝐼):𝐼–1-1→𝐼)) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢ (𝐻:𝐼–1-1→𝐼 ↔ ( I ↾ 𝐼):𝐼–1-1→𝐼) |
18 | 17 | biimpri 231 |
. . . . 5
⊢ (( I
↾ 𝐼):𝐼–1-1→𝐼 → 𝐻:𝐼–1-1→𝐼) |
19 | | fimass 6525 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝐴) ⊆ 𝐵) |
20 | 9, 19 | eqsstrid 3925 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐼 ⊆ 𝐵) |
21 | | f1ss 6580 |
. . . . 5
⊢ ((𝐻:𝐼–1-1→𝐼 ∧ 𝐼 ⊆ 𝐵) → 𝐻:𝐼–1-1→𝐵) |
22 | 18, 20, 21 | syl2an 599 |
. . . 4
⊢ ((( I
↾ 𝐼):𝐼–1-1→𝐼 ∧ 𝐹:𝐴⟶𝐵) → 𝐻:𝐼–1-1→𝐵) |
23 | 22 | ex 416 |
. . 3
⊢ (( I
↾ 𝐼):𝐼–1-1→𝐼 → (𝐹:𝐴⟶𝐵 → 𝐻:𝐼–1-1→𝐵)) |
24 | 13, 14, 23 | mp2b 10 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → 𝐻:𝐼–1-1→𝐵) |
25 | 15 | fveq1i 6675 |
. . . . 5
⊢ (𝐻‘(𝐹‘𝑥)) = (( I ↾ 𝐼)‘(𝐹‘𝑥)) |
26 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 𝐴) |
27 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
28 | 26, 27, 27 | fnfvimad 7007 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐹 “ 𝐴)) |
29 | 28, 9 | eleqtrrdi 2844 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐼) |
30 | | fvresi 6945 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ 𝐼 → (( I ↾ 𝐼)‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (( I ↾ 𝐼)‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
32 | 25, 31 | syl5eq 2785 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐻‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
33 | 32 | mpteq2dva 5125 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ 𝐴 ↦ (𝐻‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
34 | 2 | coeq2i 5703 |
. . . 4
⊢ (𝐻 ∘ 𝐺) = (𝐻 ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
35 | | f1of 6618 |
. . . . . . . 8
⊢ (( I
↾ 𝐼):𝐼–1-1-onto→𝐼 → ( I ↾ 𝐼):𝐼⟶𝐼) |
36 | 13, 35 | ax-mp 5 |
. . . . . . 7
⊢ ( I
↾ 𝐼):𝐼⟶𝐼 |
37 | 15 | feq1i 6495 |
. . . . . . 7
⊢ (𝐻:𝐼⟶𝐼 ↔ ( I ↾ 𝐼):𝐼⟶𝐼) |
38 | 36, 37 | mpbir 234 |
. . . . . 6
⊢ 𝐻:𝐼⟶𝐼 |
39 | 38 | a1i 11 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐻:𝐼⟶𝐼) |
40 | 39, 29 | cofmpt 6904 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (𝐻 ∘ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐻‘(𝐹‘𝑥)))) |
41 | 34, 40 | syl5eq 2785 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (𝐻 ∘ 𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐻‘(𝐹‘𝑥)))) |
42 | 33, 41, 5 | 3eqtr4rd 2784 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = (𝐻 ∘ 𝐺)) |
43 | 12, 24, 42 | 3jca 1129 |
1
⊢ (𝐹:𝐴⟶𝐵 → (𝐺:𝐴–onto→𝐼 ∧ 𝐻:𝐼–1-1→𝐵 ∧ 𝐹 = (𝐻 ∘ 𝐺))) |