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 x B C G x A B C B A F G x A C

Proof

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