Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . 3
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
𝐴 ∈
Fin) |
2 | | dfss3 3558 |
. . . . 5
⊢ (𝐴 ⊆ ∪ 𝐵
↔ ∀𝑥 ∈
𝐴 𝑥 ∈ ∪ 𝐵) |
3 | | eluni2 4376 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝐵
↔ ∃𝑧 ∈
𝐵 𝑥 ∈ 𝑧) |
4 | 3 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
5 | 2, 4 | sylbb 208 |
. . . 4
⊢ (𝐴 ⊆ ∪ 𝐵
→ ∀𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
6 | 5 | adantr 480 |
. . 3
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
7 | | eleq2 2677 |
. . . 4
⊢ (𝑧 = (𝑓‘𝑥) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑓‘𝑥))) |
8 | 7 | ac6sfi 8089 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) |
9 | 1, 6, 8 | syl2anc 691 |
. 2
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) |
10 | | fimass 5994 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ⊆ 𝐵) |
11 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
12 | 11 | imaex 6996 |
. . . . . . 7
⊢ (𝑓 “ 𝐴) ∈ V |
13 | 12 | elpw 4114 |
. . . . . 6
⊢ ((𝑓 “ 𝐴) ∈ 𝒫 𝐵 ↔ (𝑓 “ 𝐴) ⊆ 𝐵) |
14 | 10, 13 | sylibr 223 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
15 | 14 | ad2antrl 760 |
. . . 4
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
16 | | ffun 5961 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
17 | 16 | ad2antrl 760 |
. . . . 5
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → Fun 𝑓) |
18 | | simplr 788 |
. . . . 5
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → 𝐴 ∈ Fin) |
19 | | imafi 8142 |
. . . . 5
⊢ ((Fun
𝑓 ∧ 𝐴 ∈ Fin) → (𝑓 “ 𝐴) ∈ Fin) |
20 | 17, 18, 19 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ Fin) |
21 | 15, 20 | elind 3760 |
. . 3
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin)) |
22 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑓 Fn 𝐴) |
24 | | ssid 3587 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ 𝐴 |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ 𝐴) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
27 | | fnfvima 6400 |
. . . . . . . . . 10
⊢ ((𝑓 Fn 𝐴 ∧ 𝐴 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ (𝑓 “ 𝐴)) |
28 | 23, 25, 26, 27 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ (𝑓 “ 𝐴)) |
29 | | elssuni 4403 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) ∈ (𝑓 “ 𝐴) → (𝑓‘𝑥) ⊆ ∪ (𝑓 “ 𝐴)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ⊆ ∪ (𝑓 “ 𝐴)) |
31 | 30 | sseld 3567 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝑓‘𝑥) → 𝑥 ∈ ∪ (𝑓 “ 𝐴))) |
32 | 31 | ralimdva 2945 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥) → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴))) |
33 | 32 | imp 444 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥)) → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴)) |
34 | | dfss3 3558 |
. . . . 5
⊢ (𝐴 ⊆ ∪ (𝑓
“ 𝐴) ↔
∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴)) |
35 | 33, 34 | sylibr 223 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥)) → 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) |
36 | 35 | adantl 481 |
. . 3
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) |
37 | | unieq 4380 |
. . . . 5
⊢ (𝑐 = (𝑓 “ 𝐴) → ∪ 𝑐 = ∪
(𝑓 “ 𝐴)) |
38 | 37 | sseq2d 3596 |
. . . 4
⊢ (𝑐 = (𝑓 “ 𝐴) → (𝐴 ⊆ ∪ 𝑐 ↔ 𝐴 ⊆ ∪ (𝑓 “ 𝐴))) |
39 | 38 | rspcev 3282 |
. . 3
⊢ (((𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |
40 | 21, 36, 39 | syl2anc 691 |
. 2
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |
41 | 9, 40 | exlimddv 1850 |
1
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∃𝑐 ∈ (𝒫
𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |