Theorem uniimaelsetpreimafv

Description: The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024) (Revised by AV, 22-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion	uniimaelsetpreimafv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑆 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2	1	0nelsetpreimafv	⊢ ( 𝐹 Fn 𝐴 → ∅ ∉ 𝑃 )
3		elnelne2	⊢ ( ( 𝑆 ∈ 𝑃 ∧ ∅ ∉ 𝑃 ) → 𝑆 ≠ ∅ )
4		n0	⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑆 )
5	3 4	sylib	⊢ ( ( 𝑆 ∈ 𝑃 ∧ ∅ ∉ 𝑃 ) → ∃ 𝑦 𝑦 ∈ 𝑆 )
6	5	expcom	⊢ ( ∅ ∉ 𝑃 → ( 𝑆 ∈ 𝑃 → ∃ 𝑦 𝑦 ∈ 𝑆 ) )
7	2 6	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝑆 ∈ 𝑃 → ∃ 𝑦 𝑦 ∈ 𝑆 ) )
8	7	imp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∃ 𝑦 𝑦 ∈ 𝑆 )
9	1	imaelsetpreimafv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 “ 𝑆 ) = { ( 𝐹 ‘ 𝑦 ) } )
10	9	3expa	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 “ 𝑆 ) = { ( 𝐹 ‘ 𝑦 ) } )
11	10	unieqd	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → ∪ ( 𝐹 “ 𝑆 ) = ∪ { ( 𝐹 ‘ 𝑦 ) } )
12		fvex	⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
13	12	unisn	⊢ ∪ { ( 𝐹 ‘ 𝑦 ) } = ( 𝐹 ‘ 𝑦 )
14	11 13	eqtrdi	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → ∪ ( 𝐹 “ 𝑆 ) = ( 𝐹 ‘ 𝑦 ) )
15		dffn3	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
16	15	biimpi	⊢ ( 𝐹 Fn 𝐴 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
17	16	ad2antrr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
18	1	elsetpreimafvssdm	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → 𝑆 ⊆ 𝐴 )
19	18	sselda	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐴 )
20	17 19	ffvelrnd	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
21	14 20	eqeltrd	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑆 ) → ∪ ( 𝐹 “ 𝑆 ) ∈ ran 𝐹 )
22	8 21	exlimddv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑆 ) ∈ ran 𝐹 )