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 ) 𝐴 ⊆ ∪ 𝑐 )