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∈BC∧G∈⨉x∈A∖BC∧B⊆A→F∪G∈⨉x∈AC

Proof

Step Hyp Ref Expression
1 unexg ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC→F∪G∈V
2 1 3adant3 ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→F∪G∈V
3 ixpfn ⊢G∈⨉x∈A∖BC→GFnA∖B
4 ixpfn ⊢F∈⨉x∈BC→FFnB
5 3simpa ⊢GFnA∖B∧FFnB∧B⊆A→GFnA∖B∧FFnB
6 5 ancomd ⊢GFnA∖B∧FFnB∧B⊆A→FFnB∧GFnA∖B
7 disjdif ⊢B∩A∖B=∅
8 fnun ⊢FFnB∧GFnA∖B∧B∩A∖B=∅→F∪GFnB∪A∖B
9 6 7 8 sylancl ⊢GFnA∖B∧FFnB∧B⊆A→F∪GFnB∪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 ⊢GFnA∖B∧FFnB∧B⊆A→A=B∪A∖B
14 13 fneq2d ⊢GFnA∖B∧FFnB∧B⊆A→F∪GFnA↔F∪GFnB∪A∖B
15 9 14 mpbird ⊢GFnA∖B∧FFnB∧B⊆A→F∪GFnA
16 15 3exp ⊢GFnA∖B→FFnB→B⊆A→F∪GFnA
17 3 4 16 syl2imc ⊢F∈⨉x∈BC→G∈⨉x∈A∖BC→B⊆A→F∪GFnA
18 17 3imp ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→F∪GFnA
19 elixp2 ⊢F∈⨉x∈BC↔F∈V∧FFnB∧∀x∈BF⁡x∈C
20 19 simp3bi ⊢F∈⨉x∈BC→∀x∈BF⁡x∈C
21 fndm ⊢GFnA∖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 ⊢GFnA∖B→x∈B→G⁡x=∅
29 28 ralrimiv ⊢GFnA∖B→∀x∈BG⁡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∈BF⁡x∈C→∀x∈BG⁡x=∅→∀x∈BF⁡x∪G⁡x∈C
40 20 29 39 syl2imc ⊢GFnA∖B→F∈⨉x∈BC→∀x∈BF⁡x∪G⁡x∈C
41 3 40 syl ⊢G∈⨉x∈A∖BC→F∈⨉x∈BC→∀x∈BF⁡x∪G⁡x∈C
42 41 impcom ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC→∀x∈BF⁡x∪G⁡x∈C
43 elixp2 ⊢G∈⨉x∈A∖BC↔G∈V∧GFnA∖B∧∀x∈A∖BG⁡x∈C
44 43 simp3bi ⊢G∈⨉x∈A∖BC→∀x∈A∖BG⁡x∈C
45 fndm ⊢FFnB→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 ⊢FFnB→x∈A∖B→F⁡x=∅
53 52 ralrimiv ⊢FFnB→∀x∈A∖BF⁡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∖BG⁡x∈C→∀x∈A∖BF⁡x=∅→∀x∈A∖BF⁡x∪G⁡x∈C
67 44 53 66 syl2imc ⊢FFnB→G∈⨉x∈A∖BC→∀x∈A∖BF⁡x∪G⁡x∈C
68 4 67 syl ⊢F∈⨉x∈BC→G∈⨉x∈A∖BC→∀x∈A∖BF⁡x∪G⁡x∈C
69 68 imp ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC→∀x∈A∖BF⁡x∪G⁡x∈C
70 ralunb ⊢∀x∈B∪A∖BF⁡x∪G⁡x∈C↔∀x∈BF⁡x∪G⁡x∈C∧∀x∈A∖BF⁡x∪G⁡x∈C
71 42 69 70 sylanbrc ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC→∀x∈B∪A∖BF⁡x∪G⁡x∈C
72 71 ex ⊢F∈⨉x∈BC→G∈⨉x∈A∖BC→∀x∈B∪A∖BF⁡x∪G⁡x∈C
73 raleq ⊢A=B∪A∖B→∀x∈AF⁡x∪G⁡x∈C↔∀x∈B∪A∖BF⁡x∪G⁡x∈C
74 73 imbi2d ⊢A=B∪A∖B→G∈⨉x∈A∖BC→∀x∈AF⁡x∪G⁡x∈C↔G∈⨉x∈A∖BC→∀x∈B∪A∖BF⁡x∪G⁡x∈C
75 72 74 imbitrrid ⊢A=B∪A∖B→F∈⨉x∈BC→G∈⨉x∈A∖BC→∀x∈AF⁡x∪G⁡x∈C
76 75 eqcoms ⊢B∪A∖B=A→F∈⨉x∈BC→G∈⨉x∈A∖BC→∀x∈AF⁡x∪G⁡x∈C
77 10 76 sylbi ⊢B⊆A→F∈⨉x∈BC→G∈⨉x∈A∖BC→∀x∈AF⁡x∪G⁡x∈C
78 77 3imp231 ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→∀x∈AF⁡x∪G⁡x∈C
79 df-fn ⊢GFnA∖B↔Fun⁡G∧dom⁡G=A∖B
80 df-fn ⊢FFnB↔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∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
93 92 3exp ⊢Fun⁡F∧dom⁡F=B→Fun⁡G∧dom⁡G=A∖B→B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
94 80 93 sylbi ⊢FFnB→Fun⁡G∧dom⁡G=A∖B→B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
95 94 com12 ⊢Fun⁡G∧dom⁡G=A∖B→FFnB→B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
96 79 95 sylbi ⊢GFnA∖B→FFnB→B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
97 3 4 96 syl2imc ⊢F∈⨉x∈BC→G∈⨉x∈A∖BC→B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
98 97 3imp ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→∀x∈AF∪G⁡x∈C↔∀x∈AF⁡x∪G⁡x∈C
99 78 98 mpbird ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→∀x∈AF∪G⁡x∈C
100 elixp2 ⊢F∪G∈⨉x∈AC↔F∪G∈V∧F∪GFnA∧∀x∈AF∪G⁡x∈C
101 2 18 99 100 syl3anbrc ⊢F∈⨉x∈BC∧G∈⨉x∈A∖BC∧B⊆A→F∪G∈⨉x∈AC