Metamath Proof Explorer

Theorem undifixp

Description: Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011)

Ref Expression
Assertion undifixp 
|- ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> ( F u. G ) e. X_ x e. A C )

Proof

Step Hyp Ref Expression
1 unexg 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C ) -> ( F u. G ) e. _V )
2 1 3adant3 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> ( F u. G ) e. _V )
3 ixpfn 
 |-  ( G e. X_ x e. ( A \ B ) C -> G Fn ( A \ B ) )
4 ixpfn 
 |-  ( F e. X_ x e. B C -> F Fn B )
5 3simpa 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> ( G Fn ( A \ B ) /\ F Fn B ) )
6 5 ancomd 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> ( F Fn B /\ G Fn ( A \ B ) ) )
7 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
8 fnun 
 |-  ( ( ( F Fn B /\ G Fn ( A \ B ) ) /\ ( B i^i ( A \ B ) ) = (/) ) -> ( F u. G ) Fn ( B u. ( A \ B ) ) )
9 6 7 8 sylancl 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> ( F u. G ) Fn ( B u. ( A \ B ) ) )
10 undif 
 |-  ( B C_ A <-> ( B u. ( A \ B ) ) = A )
11 10 biimpi 
 |-  ( B C_ A -> ( B u. ( A \ B ) ) = A )
12 11 eqcomd 
 |-  ( B C_ A -> A = ( B u. ( A \ B ) ) )
13 12 3ad2ant3 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> A = ( B u. ( A \ B ) ) )
14 13 fneq2d 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> ( ( F u. G ) Fn A <-> ( F u. G ) Fn ( B u. ( A \ B ) ) ) )
15 9 14 mpbird 
 |-  ( ( G Fn ( A \ B ) /\ F Fn B /\ B C_ A ) -> ( F u. G ) Fn A )
16 15 3exp 
 |-  ( G Fn ( A \ B ) -> ( F Fn B -> ( B C_ A -> ( F u. G ) Fn A ) ) )
17 3 4 16 syl2imc 
 |-  ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> ( B C_ A -> ( F u. G ) Fn A ) ) )
18 17 3imp 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> ( F u. G ) Fn A )
19 elixp2 
 |-  ( F e. X_ x e. B C <-> ( F e. _V /\ F Fn B /\ A. x e. B ( F ` x ) e. C ) )
20 19 simp3bi 
 |-  ( F e. X_ x e. B C -> A. x e. B ( F ` x ) e. C )
21 fndm 
 |-  ( G Fn ( A \ B ) -> dom G = ( A \ B ) )
22 elndif 
 |-  ( x e. B -> -. x e. ( A \ B ) )
23 eleq2 
 |-  ( ( A \ B ) = dom G -> ( x e. ( A \ B ) <-> x e. dom G ) )
24 23 notbid 
 |-  ( ( A \ B ) = dom G -> ( -. x e. ( A \ B ) <-> -. x e. dom G ) )
25 24 eqcoms 
 |-  ( dom G = ( A \ B ) -> ( -. x e. ( A \ B ) <-> -. x e. dom G ) )
26 ndmfv 
 |-  ( -. x e. dom G -> ( G ` x ) = (/) )
27 25 26 syl6bi 
 |-  ( dom G = ( A \ B ) -> ( -. x e. ( A \ B ) -> ( G ` x ) = (/) ) )
28 21 22 27 syl2im 
 |-  ( G Fn ( A \ B ) -> ( x e. B -> ( G ` x ) = (/) ) )
29 28 ralrimiv 
 |-  ( G Fn ( A \ B ) -> A. x e. B ( G ` x ) = (/) )
30 uneq2 
 |-  ( ( G ` x ) = (/) -> ( ( F ` x ) u. ( G ` x ) ) = ( ( F ` x ) u. (/) ) )
31 un0 
 |-  ( ( F ` x ) u. (/) ) = ( F ` x )
32 eqtr 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( ( F ` x ) u. (/) ) /\ ( ( F ` x ) u. (/) ) = ( F ` x ) ) -> ( ( F ` x ) u. ( G ` x ) ) = ( F ` x ) )
33 eleq1 
 |-  ( ( F ` x ) = ( ( F ` x ) u. ( G ` x ) ) -> ( ( F ` x ) e. C <-> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
34 33 biimpd 
 |-  ( ( F ` x ) = ( ( F ` x ) u. ( G ` x ) ) -> ( ( F ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
35 34 eqcoms 
 |-  ( ( ( F ` x ) u. ( G ` x ) ) = ( F ` x ) -> ( ( F ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
36 32 35 syl 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( ( F ` x ) u. (/) ) /\ ( ( F ` x ) u. (/) ) = ( F ` x ) ) -> ( ( F ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
37 30 31 36 sylancl 
 |-  ( ( G ` x ) = (/) -> ( ( F ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
38 37 com12 
 |-  ( ( F ` x ) e. C -> ( ( G ` x ) = (/) -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
39 38 ral2imi 
 |-  ( A. x e. B ( F ` x ) e. C -> ( A. x e. B ( G ` x ) = (/) -> A. x e. B ( ( F ` x ) u. ( G ` x ) ) e. C ) )
40 20 29 39 syl2imc 
 |-  ( G Fn ( A \ B ) -> ( F e. X_ x e. B C -> A. x e. B ( ( F ` x ) u. ( G ` x ) ) e. C ) )
41 3 40 syl 
 |-  ( G e. X_ x e. ( A \ B ) C -> ( F e. X_ x e. B C -> A. x e. B ( ( F ` x ) u. ( G ` x ) ) e. C ) )
42 41 impcom 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C ) -> A. x e. B ( ( F ` x ) u. ( G ` x ) ) e. C )
43 elixp2 
 |-  ( G e. X_ x e. ( A \ B ) C <-> ( G e. _V /\ G Fn ( A \ B ) /\ A. x e. ( A \ B ) ( G ` x ) e. C ) )
44 43 simp3bi 
 |-  ( G e. X_ x e. ( A \ B ) C -> A. x e. ( A \ B ) ( G ` x ) e. C )
45 fndm 
 |-  ( F Fn B -> dom F = B )
46 eldifn 
 |-  ( x e. ( A \ B ) -> -. x e. B )
47 eleq2 
 |-  ( B = dom F -> ( x e. B <-> x e. dom F ) )
48 47 notbid 
 |-  ( B = dom F -> ( -. x e. B <-> -. x e. dom F ) )
49 ndmfv 
 |-  ( -. x e. dom F -> ( F ` x ) = (/) )
50 48 49 syl6bi 
 |-  ( B = dom F -> ( -. x e. B -> ( F ` x ) = (/) ) )
51 50 eqcoms 
 |-  ( dom F = B -> ( -. x e. B -> ( F ` x ) = (/) ) )
52 45 46 51 syl2im 
 |-  ( F Fn B -> ( x e. ( A \ B ) -> ( F ` x ) = (/) ) )
53 52 ralrimiv 
 |-  ( F Fn B -> A. x e. ( A \ B ) ( F ` x ) = (/) )
54 uneq1 
 |-  ( ( F ` x ) = (/) -> ( ( F ` x ) u. ( G ` x ) ) = ( (/) u. ( G ` x ) ) )
55 uncom 
 |-  ( (/) u. ( G ` x ) ) = ( ( G ` x ) u. (/) )
56 eqtr 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( (/) u. ( G ` x ) ) /\ ( (/) u. ( G ` x ) ) = ( ( G ` x ) u. (/) ) ) -> ( ( F ` x ) u. ( G ` x ) ) = ( ( G ` x ) u. (/) ) )
57 un0 
 |-  ( ( G ` x ) u. (/) ) = ( G ` x )
58 eqtr 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( ( G ` x ) u. (/) ) /\ ( ( G ` x ) u. (/) ) = ( G ` x ) ) -> ( ( F ` x ) u. ( G ` x ) ) = ( G ` x ) )
59 eleq1 
 |-  ( ( G ` x ) = ( ( F ` x ) u. ( G ` x ) ) -> ( ( G ` x ) e. C <-> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
60 59 biimpd 
 |-  ( ( G ` x ) = ( ( F ` x ) u. ( G ` x ) ) -> ( ( G ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
61 60 eqcoms 
 |-  ( ( ( F ` x ) u. ( G ` x ) ) = ( G ` x ) -> ( ( G ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
62 58 61 syl 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( ( G ` x ) u. (/) ) /\ ( ( G ` x ) u. (/) ) = ( G ` x ) ) -> ( ( G ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
63 56 57 62 sylancl 
 |-  ( ( ( ( F ` x ) u. ( G ` x ) ) = ( (/) u. ( G ` x ) ) /\ ( (/) u. ( G ` x ) ) = ( ( G ` x ) u. (/) ) ) -> ( ( G ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
64 54 55 63 sylancl 
 |-  ( ( F ` x ) = (/) -> ( ( G ` x ) e. C -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
65 64 com12 
 |-  ( ( G ` x ) e. C -> ( ( F ` x ) = (/) -> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
66 65 ral2imi 
 |-  ( A. x e. ( A \ B ) ( G ` x ) e. C -> ( A. x e. ( A \ B ) ( F ` x ) = (/) -> A. x e. ( A \ B ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
67 44 53 66 syl2imc 
 |-  ( F Fn B -> ( G e. X_ x e. ( A \ B ) C -> A. x e. ( A \ B ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
68 4 67 syl 
 |-  ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> A. x e. ( A \ B ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
69 68 imp 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C ) -> A. x e. ( A \ B ) ( ( F ` x ) u. ( G ` x ) ) e. C )
70 ralunb 
 |-  ( A. x e. ( B u. ( A \ B ) ) ( ( F ` x ) u. ( G ` x ) ) e. C <-> ( A. x e. B ( ( F ` x ) u. ( G ` x ) ) e. C /\ A. x e. ( A \ B ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
71 42 69 70 sylanbrc 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C ) -> A. x e. ( B u. ( A \ B ) ) ( ( F ` x ) u. ( G ` x ) ) e. C )
72 71 ex 
 |-  ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> A. x e. ( B u. ( A \ B ) ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
73 raleq 
 |-  ( A = ( B u. ( A \ B ) ) -> ( A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C <-> A. x e. ( B u. ( A \ B ) ) ( ( F ` x ) u. ( G ` x ) ) e. C ) )
74 73 imbi2d 
 |-  ( A = ( B u. ( A \ B ) ) -> ( ( G e. X_ x e. ( A \ B ) C -> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) <-> ( G e. X_ x e. ( A \ B ) C -> A. x e. ( B u. ( A \ B ) ) ( ( F ` x ) u. ( G ` x ) ) e. C ) ) )
75 72 74 syl5ibr 
 |-  ( A = ( B u. ( A \ B ) ) -> ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) )
76 75 eqcoms 
 |-  ( ( B u. ( A \ B ) ) = A -> ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) )
77 10 76 sylbi 
 |-  ( B C_ A -> ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) )
78 77 3imp231 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C )
79 df-fn 
 |-  ( G Fn ( A \ B ) <-> ( Fun G /\ dom G = ( A \ B ) ) )
80 df-fn 
 |-  ( F Fn B <-> ( Fun F /\ dom F = B ) )
81 simpl 
 |-  ( ( Fun F /\ dom F = B ) -> Fun F )
82 simpl 
 |-  ( ( Fun G /\ dom G = ( A \ B ) ) -> Fun G )
83 81 82 anim12i 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) ) -> ( Fun F /\ Fun G ) )
84 83 3adant3 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) /\ B C_ A ) -> ( Fun F /\ Fun G ) )
85 ineq12 
 |-  ( ( dom F = B /\ dom G = ( A \ B ) ) -> ( dom F i^i dom G ) = ( B i^i ( A \ B ) ) )
86 85 7 eqtrdi 
 |-  ( ( dom F = B /\ dom G = ( A \ B ) ) -> ( dom F i^i dom G ) = (/) )
87 86 ad2ant2l 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) ) -> ( dom F i^i dom G ) = (/) )
88 87 3adant3 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) /\ B C_ A ) -> ( dom F i^i dom G ) = (/) )
89 fvun 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) ` x ) = ( ( F ` x ) u. ( G ` x ) ) )
90 84 88 89 syl2anc 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) /\ B C_ A ) -> ( ( F u. G ) ` x ) = ( ( F ` x ) u. ( G ` x ) ) )
91 90 eleq1d 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) /\ B C_ A ) -> ( ( ( F u. G ) ` x ) e. C <-> ( ( F ` x ) u. ( G ` x ) ) e. C ) )
92 91 ralbidv 
 |-  ( ( ( Fun F /\ dom F = B ) /\ ( Fun G /\ dom G = ( A \ B ) ) /\ B C_ A ) -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) )
93 92 3exp 
 |-  ( ( Fun F /\ dom F = B ) -> ( ( Fun G /\ dom G = ( A \ B ) ) -> ( B C_ A -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) ) )
94 80 93 sylbi 
 |-  ( F Fn B -> ( ( Fun G /\ dom G = ( A \ B ) ) -> ( B C_ A -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) ) )
95 94 com12 
 |-  ( ( Fun G /\ dom G = ( A \ B ) ) -> ( F Fn B -> ( B C_ A -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) ) )
96 79 95 sylbi 
 |-  ( G Fn ( A \ B ) -> ( F Fn B -> ( B C_ A -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) ) )
97 3 4 96 syl2imc 
 |-  ( F e. X_ x e. B C -> ( G e. X_ x e. ( A \ B ) C -> ( B C_ A -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) ) ) )
98 97 3imp 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> ( A. x e. A ( ( F u. G ) ` x ) e. C <-> A. x e. A ( ( F ` x ) u. ( G ` x ) ) e. C ) )
99 78 98 mpbird 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> A. x e. A ( ( F u. G ) ` x ) e. C )
100 elixp2 
 |-  ( ( F u. G ) e. X_ x e. A C <-> ( ( F u. G ) e. _V /\ ( F u. G ) Fn A /\ A. x e. A ( ( F u. G ) ` x ) e. C ) )
101 2 18 99 100 syl3anbrc 
 |-  ( ( F e. X_ x e. B C /\ G e. X_ x e. ( A \ B ) C /\ B C_ A ) -> ( F u. G ) e. X_ x e. A C )