Metamath Proof Explorer

Theorem undifixp

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

Ref Expression
Assertion undifixp ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) ∈ X 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 unexg ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) → ( 𝐹 ∪ 𝐺 ) ∈ V )
2 1 3adant3 ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) ∈ V )
3 ixpfn ⊢ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → 𝐺 Fn ( 𝐴 ∖ 𝐵 ) )
4 ixpfn ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → 𝐹 Fn 𝐵 )
5 3simpa ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ) )
6 5 ancomd ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 Fn 𝐵 ∧ 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ) )
7 disjdif ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
8 fnun ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ) ∧ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
9 6 7 8 sylancl ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
10 undif ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
11 10 biimpi ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
12 11 eqcomd ⊢ ( 𝐵 ⊆ 𝐴 → 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
13 12 3ad2ant3 ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) )
14 13 fneq2d ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ∪ 𝐺 ) Fn 𝐴 ↔ ( 𝐹 ∪ 𝐺 ) Fn ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) )
15 9 14 mpbird ⊢ ( ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) Fn 𝐴 )
16 15 3exp ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → ( 𝐹 Fn 𝐵 → ( 𝐵 ⊆ 𝐴 → ( 𝐹 ∪ 𝐺 ) Fn 𝐴 ) ) )
17 3 4 16 syl2imc ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ( 𝐵 ⊆ 𝐴 → ( 𝐹 ∪ 𝐺 ) Fn 𝐴 ) ) )
18 17 3imp ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) Fn 𝐴 )
19 elixp2 ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ) )
20 19 simp3bi ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
21 fndm ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → dom 𝐺 = ( 𝐴 ∖ 𝐵 ) )
22 elndif ⊢ ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
23 eleq2 ⊢ ( ( 𝐴 ∖ 𝐵 ) = dom 𝐺 → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ 𝑥 ∈ dom 𝐺 ) )
24 23 notbid ⊢ ( ( 𝐴 ∖ 𝐵 ) = dom 𝐺 → ( ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ¬ 𝑥 ∈ dom 𝐺 ) )
25 24 eqcoms ⊢ ( dom 𝐺 = ( 𝐴 ∖ 𝐵 ) → ( ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ¬ 𝑥 ∈ dom 𝐺 ) )
26 ndmfv ⊢ ( ¬ 𝑥 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑥 ) = ∅ )
27 25 26 biimtrdi ⊢ ( dom 𝐺 = ( 𝐴 ∖ 𝐵 ) → ( ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ∅ ) )
28 21 22 27 syl2im ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( 𝐺 ‘ 𝑥 ) = ∅ ) )
29 28 ralrimiv ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 𝐺 ‘ 𝑥 ) = ∅ )
30 uneq2 ⊢ ( ( 𝐺 ‘ 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) )
31 un0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐹 ‘ 𝑥 )
32 eqtr ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
33 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
34 33 biimpd ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
35 34 eqcoms ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
36 32 35 syl ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
37 30 31 36 sylancl ⊢ ( ( 𝐺 ‘ 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
38 37 com12 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐺 ‘ 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
39 38 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐺 ‘ 𝑥 ) = ∅ → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
40 20 29 39 syl2imc ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
41 3 40 syl ⊢ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
42 41 impcom ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 )
43 elixp2 ⊢ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 ) )
44 43 simp3bi ⊢ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
45 fndm ⊢ ( 𝐹 Fn 𝐵 → dom 𝐹 = 𝐵 )
46 eldifn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 𝑥 ∈ 𝐵 )
47 eleq2 ⊢ ( 𝐵 = dom 𝐹 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹 ) )
48 47 notbid ⊢ ( 𝐵 = dom 𝐹 → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹 ) )
49 ndmfv ⊢ ( ¬ 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) = ∅ )
50 48 49 biimtrdi ⊢ ( 𝐵 = dom 𝐹 → ( ¬ 𝑥 ∈ 𝐵 → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
51 50 eqcoms ⊢ ( dom 𝐹 = 𝐵 → ( ¬ 𝑥 ∈ 𝐵 → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
52 45 46 51 syl2im ⊢ ( 𝐹 Fn 𝐵 → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
53 52 ralrimiv ⊢ ( 𝐹 Fn 𝐵 → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = ∅ )
54 uneq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) )
55 uncom ⊢ ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ )
56 eqtr ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) ∧ ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) ) → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) )
57 un0 ⊢ ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑥 )
58 eqtr ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) ∧ ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
59 eleq1 ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
60 59 biimpd ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
61 60 eqcoms ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
62 58 61 syl ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) ∧ ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑥 ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
63 56 57 62 sylancl ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) ∧ ( ∅ ∪ ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑥 ) ∪ ∅ ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
64 54 55 63 sylancl ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
65 64 com12 ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
66 65 ral2imi ⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = ∅ → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
67 44 53 66 syl2imc ⊢ ( 𝐹 Fn 𝐵 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
68 4 67 syl ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
69 68 imp ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) → ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 )
70 ralunb ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
71 42 69 70 sylanbrc ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ) → ∀ 𝑥 ∈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 )
72 71 ex ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
73 raleq ⊢ ( 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
74 73 imbi2d ⊢ ( 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) → ( ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ↔ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) )
75 72 74 imbitrrid ⊢ ( 𝐴 = ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) → ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) )
76 75 eqcoms ⊢ ( ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 → ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) )
77 10 76 sylbi ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) )
78 77 3imp231 ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 )
79 df-fn ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) ↔ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) )
80 df-fn ⊢ ( 𝐹 Fn 𝐵 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) )
81 simpl ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) → Fun 𝐹 )
82 simpl ⊢ ( ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → Fun 𝐺 )
83 81 82 anim12i ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )
84 83 3adant3 ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ∧ 𝐵 ⊆ 𝐴 ) → ( Fun 𝐹 ∧ Fun 𝐺 ) )
85 ineq12 ⊢ ( ( dom 𝐹 = 𝐵 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) )
86 85 7 eqtrdi ⊢ ( ( dom 𝐹 = 𝐵 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ )
87 86 ad2ant2l ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ )
88 87 3adant3 ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ∧ 𝐵 ⊆ 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = ∅ )
89 fvun ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) )
90 84 88 89 syl2anc ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) )
91 90 eleq1d ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
92 91 ralbidv ⊢ ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ∧ ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
93 92 3exp ⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) → ( ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) ) )
94 80 93 sylbi ⊢ ( 𝐹 Fn 𝐵 → ( ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) ) )
95 94 com12 ⊢ ( ( Fun 𝐺 ∧ dom 𝐺 = ( 𝐴 ∖ 𝐵 ) ) → ( 𝐹 Fn 𝐵 → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) ) )
96 79 95 sylbi ⊢ ( 𝐺 Fn ( 𝐴 ∖ 𝐵 ) → ( 𝐹 Fn 𝐵 → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) ) )
97 3 4 96 syl2imc ⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 → ( 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 → ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) ) ) )
98 97 3imp ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ∪ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐶 ) )
99 78 98 mpbird ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 )
100 elixp2 ⊢ ( ( 𝐹 ∪ 𝐺 ) ∈ X 𝑥 ∈ 𝐴 𝐶 ↔ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ ( 𝐹 ∪ 𝐺 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∪ 𝐺 ) ‘ 𝑥 ) ∈ 𝐶 ) )
101 2 18 99 100 syl3anbrc ⊢ ( ( 𝐹 ∈ X 𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝐶 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 ∪ 𝐺 ) ∈ X 𝑥 ∈ 𝐴 𝐶 )