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 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𝐵 𝐵 = 𝑥𝐴 ( 𝐹𝑥 ) )