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 syl6eq ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑋𝐴 ) ) → ( ( 𝐹𝑋 ) ∪ ( 𝐺𝑋 ) ) = ( 𝐹𝑋 ) )
25 13 24 eqtrd ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ( ( 𝐴𝐵 ) = ∅ ∧ 𝑋𝐴 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑋 ) = ( 𝐹𝑋 ) )