Theorem founiiun

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	founiiun	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐵 = ∪ 𝑦 ∈ 𝐵 𝑦
2		foelrni	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
3		eqimss2	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
4	3	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
5	2 4	syl	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
6	5	ralrimiva	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
7		iunss2	⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
8	6 7	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
9		fof	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
10	9	ffvelrnda	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11		ssidd	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
12		sseq2	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
13	12	rspcev	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
14	10 11 13	syl2anc	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
15	14	ralrimiva	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
16		iunss2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
17	15 16	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
18	8 17	eqssd	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
19	1 18	syl5eq	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )