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

Metamath Proof Explorer

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 foelcdmi ⊢ ( ( 𝐹 : 𝐴 –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 ffvelcdmda ⊢ ( ( 𝐹 : 𝐴 –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 eqtrid ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )