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 F Fn A G Fn B A B = X A F G X = F X

Proof

Step Hyp Ref Expression
1 fnfun F Fn A Fun F
2 1 3ad2ant1 F Fn A G Fn B A B = X A Fun F
3 fnfun G Fn B Fun G
4 3 3ad2ant2 F Fn A G Fn B A B = X A Fun G
5 fndm F Fn A dom F = A
6 fndm G Fn B dom G = B
7 5 6 ineqan12d F Fn A G Fn B dom F dom G = A B
8 7 eqeq1d F Fn A G Fn B dom F dom G = A B =
9 8 biimprd F Fn A G Fn B A B = dom F dom G =
10 9 adantrd F Fn A G Fn B A B = X A dom F dom G =
11 10 3impia F Fn A G Fn B A B = X A dom F dom G =
12 fvun Fun F Fun G dom F dom G = F G X = F X G X
13 2 4 11 12 syl21anc F Fn A G Fn B A B = X A F G X = F X G X
14 disjel A B = X A ¬ X B
15 14 adantl G Fn B A B = X A ¬ X B
16 6 eleq2d G Fn B X dom G X B
17 16 adantr G Fn B A B = X A X dom G X B
18 15 17 mtbird G Fn B A B = X A ¬ X dom G
19 18 3adant1 F Fn A G Fn B A B = X A ¬ X dom G
20 ndmfv ¬ X dom G G X =
21 19 20 syl F Fn A G Fn B A B = X A G X =
22 21 uneq2d F Fn A G Fn B A B = X A F X G X = F X
23 un0 F X = F X
24 22 23 syl6eq F Fn A G Fn B A B = X A F X G X = F X
25 13 24 eqtrd F Fn A G Fn B A B = X A F G X = F X