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 syl6bi ( 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 syl6bi ( 𝐵 = 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 syl5ibr ( 𝐴 = ( 𝐵 ∪ ( 𝐴𝐵 ) ) → ( 𝐹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 𝑥𝐴 𝐶 )