Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. . 3
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
2 | | dfss3 3558 |
. . . . . 6
⊢ (𝐴 ⊆ ran 𝐹 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ ran 𝐹) |
3 | | fvelrnb 6153 |
. . . . . . 7
⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥)) |
4 | 3 | ralbidv 2969 |
. . . . . 6
⊢ (𝐹 Fn 𝐵 → (∀𝑥 ∈ 𝐴 𝑥 ∈ ran 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥)) |
5 | 2, 4 | syl5bb 271 |
. . . . 5
⊢ (𝐹 Fn 𝐵 → (𝐴 ⊆ ran 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥)) |
6 | 5 | biimpa 500 |
. . . 4
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥) |
7 | 6 | 3adant3 1074 |
. . 3
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥) |
8 | | fveq2 6103 |
. . . . 5
⊢ (𝑦 = (𝑓‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝑓‘𝑥))) |
9 | 8 | eqeq1d 2612 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑥) → ((𝐹‘𝑦) = 𝑥 ↔ (𝐹‘(𝑓‘𝑥)) = 𝑥)) |
10 | 9 | ac6sfi 8089 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐹‘𝑦) = 𝑥) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) |
11 | 1, 7, 10 | syl2anc 691 |
. 2
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) |
12 | | fimass 5994 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ⊆ 𝐵) |
13 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
14 | 13 | imaex 6996 |
. . . . . . 7
⊢ (𝑓 “ 𝐴) ∈ V |
15 | 14 | elpw 4114 |
. . . . . 6
⊢ ((𝑓 “ 𝐴) ∈ 𝒫 𝐵 ↔ (𝑓 “ 𝐴) ⊆ 𝐵) |
16 | 12, 15 | sylibr 223 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
17 | 16 | ad2antrl 760 |
. . . 4
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
18 | | ffun 5961 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
19 | 18 | ad2antrl 760 |
. . . . 5
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → Fun 𝑓) |
20 | | simpl3 1059 |
. . . . 5
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → 𝐴 ∈ Fin) |
21 | | imafi 8142 |
. . . . 5
⊢ ((Fun
𝑓 ∧ 𝐴 ∈ Fin) → (𝑓 “ 𝐴) ∈ Fin) |
22 | 19, 20, 21 | syl2anc 691 |
. . . 4
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝑓 “ 𝐴) ∈ Fin) |
23 | 17, 22 | elind 3760 |
. . 3
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin)) |
24 | | fvco3 6185 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ 𝑓)‘𝑥) = (𝐹‘(𝑓‘𝑥))) |
25 | | fvresi 6344 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑥) = 𝑥) |
26 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (( I ↾ 𝐴)‘𝑥) = 𝑥) |
27 | 24, 26 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥) ↔ (𝐹‘(𝑓‘𝑥)) = 𝑥)) |
28 | 27 | ralbidva 2968 |
. . . . . . . . 9
⊢ (𝑓:𝐴⟶𝐵 → (∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) |
29 | 28 | biimprd 237 |
. . . . . . . 8
⊢ (𝑓:𝐴⟶𝐵 → (∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥 → ∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥))) |
30 | 29 | adantl 481 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ 𝑓:𝐴⟶𝐵) → (∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥 → ∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥))) |
31 | 30 | impr 647 |
. . . . . 6
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → ∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥)) |
32 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → 𝐹 Fn 𝐵) |
33 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
34 | 33 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → 𝑓 Fn 𝐴) |
35 | | frn 5966 |
. . . . . . . . 9
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
36 | 35 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → ran 𝑓 ⊆ 𝐵) |
37 | | fnco 5913 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐵 ∧ 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵) → (𝐹 ∘ 𝑓) Fn 𝐴) |
38 | 32, 34, 36, 37 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝐹 ∘ 𝑓) Fn 𝐴) |
39 | | fnresi 5922 |
. . . . . . 7
⊢ ( I
↾ 𝐴) Fn 𝐴 |
40 | | eqfnfv 6219 |
. . . . . . 7
⊢ (((𝐹 ∘ 𝑓) Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → ((𝐹 ∘ 𝑓) = ( I ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥))) |
41 | 38, 39, 40 | sylancl 693 |
. . . . . 6
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → ((𝐹 ∘ 𝑓) = ( I ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ((𝐹 ∘ 𝑓)‘𝑥) = (( I ↾ 𝐴)‘𝑥))) |
42 | 31, 41 | mpbird 246 |
. . . . 5
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝐹 ∘ 𝑓) = ( I ↾ 𝐴)) |
43 | 42 | imaeq1d 5384 |
. . . 4
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → ((𝐹 ∘ 𝑓) “ 𝐴) = (( I ↾ 𝐴) “ 𝐴)) |
44 | | imaco 5557 |
. . . 4
⊢ ((𝐹 ∘ 𝑓) “ 𝐴) = (𝐹 “ (𝑓 “ 𝐴)) |
45 | | ssid 3587 |
. . . . 5
⊢ 𝐴 ⊆ 𝐴 |
46 | | resiima 5399 |
. . . . 5
⊢ (𝐴 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐴) = 𝐴) |
47 | 45, 46 | ax-mp 5 |
. . . 4
⊢ (( I
↾ 𝐴) “ 𝐴) = 𝐴 |
48 | 43, 44, 47 | 3eqtr3g 2667 |
. . 3
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → (𝐹 “ (𝑓 “ 𝐴)) = 𝐴) |
49 | | imaeq2 5381 |
. . . . 5
⊢ (𝑐 = (𝑓 “ 𝐴) → (𝐹 “ 𝑐) = (𝐹 “ (𝑓 “ 𝐴))) |
50 | 49 | eqeq1d 2612 |
. . . 4
⊢ (𝑐 = (𝑓 “ 𝐴) → ((𝐹 “ 𝑐) = 𝐴 ↔ (𝐹 “ (𝑓 “ 𝐴)) = 𝐴)) |
51 | 50 | rspcev 3282 |
. . 3
⊢ (((𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin) ∧ (𝐹 “ (𝑓 “ 𝐴)) = 𝐴) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴) |
52 | 23, 48, 51 | syl2anc 691 |
. 2
⊢ (((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝑓‘𝑥)) = 𝑥)) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴) |
53 | 11, 52 | exlimddv 1850 |
1
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴) |