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 biimtrdi ⊢ 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 biimtrdi ⊢ 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 imbitrrid ⊢ 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