Metamath Proof Explorer

Theorem funiunfv

Description: The indexed union of a function's values is the union of its image under the index class.

Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to F Fn A , the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion funiunfv ( Fun 𝐹 𝑥𝐴 ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )

Proof

Step Hyp Ref Expression
1 funres ( Fun 𝐹 → Fun ( 𝐹𝐴 ) )
2 1 funfnd ( Fun 𝐹 → ( 𝐹𝐴 ) Fn dom ( 𝐹𝐴 ) )
3 fniunfv ( ( 𝐹𝐴 ) Fn dom ( 𝐹𝐴 ) → 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ran ( 𝐹𝐴 ) )
4 2 3 syl ( Fun 𝐹 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ran ( 𝐹𝐴 ) )
5 undif2 ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) = ( dom ( 𝐹𝐴 ) ∪ 𝐴 )
6 dmres dom ( 𝐹𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
7 inss1 ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
8 6 7 eqsstri dom ( 𝐹𝐴 ) ⊆ 𝐴
9 ssequn1 ( dom ( 𝐹𝐴 ) ⊆ 𝐴 ↔ ( dom ( 𝐹𝐴 ) ∪ 𝐴 ) = 𝐴 )
10 8 9 mpbi ( dom ( 𝐹𝐴 ) ∪ 𝐴 ) = 𝐴
11 5 10 eqtri ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) = 𝐴
12 iuneq1 ( ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) = 𝐴 𝑥 ∈ ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = 𝑥𝐴 ( ( 𝐹𝐴 ) ‘ 𝑥 ) )
13 11 12 ax-mp 𝑥 ∈ ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = 𝑥𝐴 ( ( 𝐹𝐴 ) ‘ 𝑥 )
14 iunxun 𝑥 ∈ ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ( 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) )
15 eldifn ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) → ¬ 𝑥 ∈ dom ( 𝐹𝐴 ) )
16 ndmfv ( ¬ 𝑥 ∈ dom ( 𝐹𝐴 ) → ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ∅ )
17 15 16 syl ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) → ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ∅ )
18 17 iuneq2i 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ∅
19 iun0 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ∅ = ∅
20 18 19 eqtri 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ∅
21 20 uneq2i ( 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∪ ∅ )
22 un0 ( 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∪ ∅ ) = 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 )
23 21 22 eqtri ( 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ∪ 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) ) = 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 )
24 14 23 eqtri 𝑥 ∈ ( dom ( 𝐹𝐴 ) ∪ ( 𝐴 ∖ dom ( 𝐹𝐴 ) ) ) ( ( 𝐹𝐴 ) ‘ 𝑥 ) = 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 )
25 fvres ( 𝑥𝐴 → ( ( 𝐹𝐴 ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
26 25 iuneq2i 𝑥𝐴 ( ( 𝐹𝐴 ) ‘ 𝑥 ) = 𝑥𝐴 ( 𝐹𝑥 )
27 13 24 26 3eqtr3ri 𝑥𝐴 ( 𝐹𝑥 ) = 𝑥 ∈ dom ( 𝐹𝐴 ) ( ( 𝐹𝐴 ) ‘ 𝑥 )
28 df-ima ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
29 28 unieqi ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
30 4 27 29 3eqtr4g ( Fun 𝐹 𝑥𝐴 ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )