This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin ) → ∃ 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝐴 ⊆ ∪ 𝑐 )

Proof

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