Metamath Proof Explorer

Theorem fissuni

Description: A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion fissuni ⊢ A ⊆ ⋃ B ∧ A ∈ Fin → ∃ c ∈ 𝒫 B ∩ Fin A ⊆ ⋃ c

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ⊆ ⋃ B ∧ A ∈ Fin → A ∈ Fin
2 dfss3 ⊢ A ⊆ ⋃ B ↔ ∀ x ∈ A x ∈ ⋃ B
3 eluni2 ⊢ x ∈ ⋃ B ↔ ∃ z ∈ B x ∈ z
4 3 ralbii ⊢ ∀ x ∈ A x ∈ ⋃ B ↔ ∀ x ∈ A ∃ z ∈ B x ∈ z
5 2 4 sylbb ⊢ A ⊆ ⋃ B → ∀ x ∈ A ∃ z ∈ B x ∈ z
6 5 adantr ⊢ A ⊆ ⋃ B ∧ A ∈ Fin → ∀ x ∈ A ∃ z ∈ B x ∈ z
7 eleq2 ⊢ z = f ⁡ x → x ∈ z ↔ x ∈ f ⁡ x
8 7 ac6sfi ⊢ A ∈ Fin ∧ ∀ x ∈ A ∃ z ∈ B x ∈ z → ∃ f f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x
9 1 6 8 syl2anc ⊢ A ⊆ ⋃ B ∧ A ∈ Fin → ∃ f f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x
10 fimass ⊢ f : A ⟶ B → f A ⊆ B
11 vex ⊢ f ∈ V
12 11 imaex ⊢ f A ∈ V
13 12 elpw ⊢ f A ∈ 𝒫 B ↔ f A ⊆ B
14 10 13 sylibr ⊢ f : A ⟶ B → f A ∈ 𝒫 B
15 14 ad2antrl ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → f A ∈ 𝒫 B
16 ffun ⊢ f : A ⟶ B → Fun ⁡ f
17 16 ad2antrl ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → Fun ⁡ f
18 simplr ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → A ∈ Fin
19 imafi ⊢ Fun ⁡ f ∧ A ∈ Fin → f A ∈ Fin
20 17 18 19 syl2anc ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → f A ∈ Fin
21 15 20 elind ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → f A ∈ 𝒫 B ∩ Fin
22 ffn ⊢ f : A ⟶ B → f Fn A
23 22 adantr ⊢ f : A ⟶ B ∧ x ∈ A → f Fn A
24 ssidd ⊢ f : A ⟶ B ∧ x ∈ A → A ⊆ A
25 simpr ⊢ f : A ⟶ B ∧ x ∈ A → x ∈ A
26 fnfvima ⊢ f Fn A ∧ A ⊆ A ∧ x ∈ A → f ⁡ x ∈ f A
27 23 24 25 26 syl3anc ⊢ f : A ⟶ B ∧ x ∈ A → f ⁡ x ∈ f A
28 elssuni ⊢ f ⁡ x ∈ f A → f ⁡ x ⊆ ⋃ f A
29 27 28 syl ⊢ f : A ⟶ B ∧ x ∈ A → f ⁡ x ⊆ ⋃ f A
30 29 sseld ⊢ f : A ⟶ B ∧ x ∈ A → x ∈ f ⁡ x → x ∈ ⋃ f A
31 30 ralimdva ⊢ f : A ⟶ B → ∀ x ∈ A x ∈ f ⁡ x → ∀ x ∈ A x ∈ ⋃ f A
32 31 imp ⊢ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → ∀ x ∈ A x ∈ ⋃ f A
33 dfss3 ⊢ A ⊆ ⋃ f A ↔ ∀ x ∈ A x ∈ ⋃ f A
34 32 33 sylibr ⊢ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → A ⊆ ⋃ f A
35 34 adantl ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → A ⊆ ⋃ f A
36 unieq ⊢ c = f A → ⋃ c = ⋃ f A
37 36 sseq2d ⊢ c = f A → A ⊆ ⋃ c ↔ A ⊆ ⋃ f A
38 37 rspcev ⊢ f A ∈ 𝒫 B ∩ Fin ∧ A ⊆ ⋃ f A → ∃ c ∈ 𝒫 B ∩ Fin A ⊆ ⋃ c
39 21 35 38 syl2anc ⊢ A ⊆ ⋃ B ∧ A ∈ Fin ∧ f : A ⟶ B ∧ ∀ x ∈ A x ∈ f ⁡ x → ∃ c ∈ 𝒫 B ∩ Fin A ⊆ ⋃ c
40 9 39 exlimddv ⊢ A ⊆ ⋃ B ∧ A ∈ Fin → ∃ c ∈ 𝒫 B ∩ Fin A ⊆ ⋃ c