Metamath Proof Explorer

Theorem fvun1

Description: The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Assertion fvun1 ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2 1 3ad2ant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → Fun 𝐹 )
3 fnfun ⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
4 3 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → Fun 𝐺 )
5 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6 fndm ⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
7 5 6 ineqan12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐵 ) )
8 7 eqeq1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
9 8 biimprd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) )
10 9 adantrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) )
11 10 3impia ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ )
12 fvun ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ∪ ( 𝐺 ‘ 𝑋 ) ) )
13 2 4 11 12 syl21anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ∪ ( 𝐺 ‘ 𝑋 ) ) )
14 disjel ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) → ¬ 𝑋 ∈ 𝐵 )
15 14 adantl ⊢ ( ( 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ¬ 𝑋 ∈ 𝐵 )
16 6 eleq2d ⊢ ( 𝐺 Fn 𝐵 → ( 𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵 ) )
17 16 adantr ⊢ ( ( 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵 ) )
18 15 17 mtbird ⊢ ( ( 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ¬ 𝑋 ∈ dom 𝐺 )
19 18 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ¬ 𝑋 ∈ dom 𝐺 )
20 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑋 ) = ∅ )
21 19 20 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑋 ) = ∅ )
22 21 uneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∪ ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) ∪ ∅ ) )
23 un0 ⊢ ( ( 𝐹 ‘ 𝑋 ) ∪ ∅ ) = ( 𝐹 ‘ 𝑋 )
24 22 23 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∪ ( 𝐺 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
25 13 24 eqtrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )