Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . 3
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
𝐴 ∈
Fin) |
2 | | dfss3 3592 |
. . . . 5
⊢ (𝐴 ⊆ ∪ 𝐵
↔ ∀𝑥 ∈
𝐴 𝑥 ∈ ∪ 𝐵) |
3 | | eluni2 4440 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝐵
↔ ∃𝑧 ∈
𝐵 𝑥 ∈ 𝑧) |
4 | 3 | ralbii 2980 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
5 | 2, 4 | sylbb 209 |
. . . 4
⊢ (𝐴 ⊆ ∪ 𝐵
→ ∀𝑥 ∈
𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) |
7 | | eleq2 2690 |
. . . 4
⊢ (𝑧 = (𝑓‘𝑥) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑓‘𝑥))) |
8 | 7 | ac6sfi 8204 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 ∈ 𝑧) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) |
9 | 1, 6, 8 | syl2anc 693 |
. 2
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) |
10 | | fimass 6081 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ⊆ 𝐵) |
11 | | vex 3203 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
12 | 11 | imaex 7104 |
. . . . . . 7
⊢ (𝑓 “ 𝐴) ∈ V |
13 | 12 | elpw 4164 |
. . . . . 6
⊢ ((𝑓 “ 𝐴) ∈ 𝒫 𝐵 ↔ (𝑓 “ 𝐴) ⊆ 𝐵) |
14 | 10, 13 | sylibr 224 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
15 | 14 | ad2antrl 764 |
. . . 4
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ 𝒫 𝐵) |
16 | | ffun 6048 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
17 | 16 | ad2antrl 764 |
. . . . 5
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → Fun 𝑓) |
18 | | simplr 792 |
. . . . 5
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → 𝐴 ∈ Fin) |
19 | | imafi 8259 |
. . . . 5
⊢ ((Fun
𝑓 ∧ 𝐴 ∈ Fin) → (𝑓 “ 𝐴) ∈ Fin) |
20 | 17, 18, 19 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ Fin) |
21 | 15, 20 | elind 3798 |
. . 3
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → (𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin)) |
22 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑓 Fn 𝐴) |
24 | | ssid 3624 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ 𝐴 |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ 𝐴) |
26 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
27 | | fnfvima 6496 |
. . . . . . . . . 10
⊢ ((𝑓 Fn 𝐴 ∧ 𝐴 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ (𝑓 “ 𝐴)) |
28 | 23, 25, 26, 27 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ (𝑓 “ 𝐴)) |
29 | | elssuni 4467 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) ∈ (𝑓 “ 𝐴) → (𝑓‘𝑥) ⊆ ∪ (𝑓 “ 𝐴)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ⊆ ∪ (𝑓 “ 𝐴)) |
31 | 30 | sseld 3602 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝑓‘𝑥) → 𝑥 ∈ ∪ (𝑓 “ 𝐴))) |
32 | 31 | ralimdva 2962 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥) → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴))) |
33 | 32 | imp 445 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥)) → ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴)) |
34 | | dfss3 3592 |
. . . . 5
⊢ (𝐴 ⊆ ∪ (𝑓
“ 𝐴) ↔
∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑓 “ 𝐴)) |
35 | 33, 34 | sylibr 224 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥)) → 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) |
36 | 35 | adantl 482 |
. . 3
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) |
37 | | unieq 4444 |
. . . . 5
⊢ (𝑐 = (𝑓 “ 𝐴) → ∪ 𝑐 = ∪
(𝑓 “ 𝐴)) |
38 | 37 | sseq2d 3633 |
. . . 4
⊢ (𝑐 = (𝑓 “ 𝐴) → (𝐴 ⊆ ∪ 𝑐 ↔ 𝐴 ⊆ ∪ (𝑓 “ 𝐴))) |
39 | 38 | rspcev 3309 |
. . 3
⊢ (((𝑓 “ 𝐴) ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 ⊆ ∪ (𝑓 “ 𝐴)) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |
40 | 21, 36, 39 | syl2anc 693 |
. 2
⊢ (((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) ∧
(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ (𝑓‘𝑥))) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |
41 | 9, 40 | exlimddv 1863 |
1
⊢ ((𝐴 ⊆ ∪ 𝐵
∧ 𝐴 ∈ Fin) →
∃𝑐 ∈ (𝒫
𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) |