Metamath Proof Explorer

Theorem suppovss

Description: A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023)

Ref Expression
Hypotheses suppovss.f 
|- F = ( x e. A , y e. B |-> C )
suppovss.g 
|- G = ( x e. A |-> ( y e. B |-> C ) )
suppovss.a 
|- ( ph -> A e. V )
suppovss.b 
|- ( ph -> B e. W )
suppovss.z 
|- ( ph -> Z e. D )
suppovss.1 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
Assertion suppovss 
|- ( ph -> ( F supp Z ) C_ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )

Proof

Step Hyp Ref Expression
1 suppovss.f 
 |-  F = ( x e. A , y e. B |-> C )
2 suppovss.g 
 |-  G = ( x e. A |-> ( y e. B |-> C ) )
3 suppovss.a 
 |-  ( ph -> A e. V )
4 suppovss.b 
 |-  ( ph -> B e. W )
5 suppovss.z 
 |-  ( ph -> Z e. D )
6 suppovss.1 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
7 6 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. B C e. D )
8 1 fmpo 
 |-  ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )
9 7 8 sylib 
 |-  ( ph -> F : ( A X. B ) --> D )
10 simpr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> z = <. x , y >. )
11 10 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = ( F ` <. x , y >. ) )
12 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
13 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> x e. ( A \ ( G supp ( B X. { Z } ) ) ) )
14 13 eldifad 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> x e. A )
15 simplr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> y e. B )
16 simplll 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ph )
17 16 14 15 6 syl12anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> C e. D )
18 1 ovmpt4g 
 |-  ( ( x e. A /\ y e. B /\ C e. D ) -> ( x F y ) = C )
19 14 15 17 18 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( x F y ) = C )
20 12 19 eqtr3id 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` <. x , y >. ) = C )
21 4 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. W )
22 21 mptexd 
 |-  ( ( ph /\ x e. A ) -> ( y e. B |-> C ) e. _V )
23 22 2 fmptd 
 |-  ( ph -> G : A --> _V )
24 ssidd 
 |-  ( ph -> ( G supp ( B X. { Z } ) ) C_ ( G supp ( B X. { Z } ) ) )
25 snex 
 |-  { Z } e. _V
26 25 a1i 
 |-  ( ph -> { Z } e. _V )
27 4 26 xpexd 
 |-  ( ph -> ( B X. { Z } ) e. _V )
28 23 24 3 27 suppssr 
 |-  ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( G ` x ) = ( B X. { Z } ) )
29 28 fveq1d 
 |-  ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( ( G ` x ) ` y ) = ( ( B X. { Z } ) ` y ) )
30 16 13 29 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = ( ( B X. { Z } ) ` y ) )
31 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
32 2 fvmpt2 
 |-  ( ( x e. A /\ ( y e. B |-> C ) e. _V ) -> ( G ` x ) = ( y e. B |-> C ) )
33 31 22 32 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = ( y e. B |-> C ) )
34 6 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. D )
35 33 34 fvmpt2d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ( G ` x ) ` y ) = C )
36 16 14 15 35 syl21anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = C )
37 16 5 syl 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> Z e. D )
38 fvconst2g 
 |-  ( ( Z e. D /\ y e. B ) -> ( ( B X. { Z } ) ` y ) = Z )
39 37 15 38 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( B X. { Z } ) ` y ) = Z )
40 30 36 39 3eqtr3d 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> C = Z )
41 11 20 40 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
42 41 adantl3r 
 |-  ( ( ( ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
43 elxp2 
 |-  ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) <-> E. x e. ( A \ ( G supp ( B X. { Z } ) ) ) E. y e. B z = <. x , y >. )
44 43 bilani 
 |-  ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> E. x e. ( A \ ( G supp ( B X. { Z } ) ) ) E. y e. B z = <. x , y >. )
45 42 44 r19.29vva 
 |-  ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> ( F ` z ) = Z )
46 45 adantlr 
 |-  ( ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> ( F ` z ) = Z )
47 simpr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> z = <. x , y >. )
48 47 fveq2d 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = ( F ` <. x , y >. ) )
49 simpllr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> x e. A )
50 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )
51 50 eldifad 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> y e. B )
52 simplll 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ph )
53 52 49 51 6 syl12anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> C e. D )
54 49 51 53 18 syl3anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( x F y ) = C )
55 12 54 eqtr3id 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` <. x , y >. ) = C )
56 52 49 51 35 syl21anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = C )
57 fvexd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ( G ` x ) ` y ) e. _V )
58 34 33 57 fmpt2d 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) : B --> _V )
59 ssiun2 
 |-  ( x e. A -> ( ( G ` x ) supp Z ) C_ U_ x e. A ( ( G ` x ) supp Z ) )
60 59 adantl 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ x e. A ( ( G ` x ) supp Z ) )
61 fveq2 
 |-  ( x = k -> ( G ` x ) = ( G ` k ) )
62 61 oveq1d 
 |-  ( x = k -> ( ( G ` x ) supp Z ) = ( ( G ` k ) supp Z ) )
63 62 cbviunv 
 |-  U_ x e. A ( ( G ` x ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z )
64 60 63 sseqtrdi 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ k e. A ( ( G ` k ) supp Z ) )
65 simpl 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ph )
66 simpr 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> k e. ( A \ ( G supp ( B X. { Z } ) ) ) )
67 66 eldifad 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> k e. A )
68 23 24 3 27 suppssr 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( G ` k ) = ( B X. { Z } ) )
69 eleq1w 
 |-  ( x = k -> ( x e. A <-> k e. A ) )
70 69 anbi2d 
 |-  ( x = k -> ( ( ph /\ x e. A ) <-> ( ph /\ k e. A ) ) )
71 61 fneq1d 
 |-  ( x = k -> ( ( G ` x ) Fn B <-> ( G ` k ) Fn B ) )
72 70 71 imbi12d 
 |-  ( x = k -> ( ( ( ph /\ x e. A ) -> ( G ` x ) Fn B ) <-> ( ( ph /\ k e. A ) -> ( G ` k ) Fn B ) ) )
73 58 ffnd 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) Fn B )
74 72 73 chvarvv 
 |-  ( ( ph /\ k e. A ) -> ( G ` k ) Fn B )
75 4 adantr 
 |-  ( ( ph /\ k e. A ) -> B e. W )
76 5 adantr 
 |-  ( ( ph /\ k e. A ) -> Z e. D )
77 fnsuppeq0 
 |-  ( ( ( G ` k ) Fn B /\ B e. W /\ Z e. D ) -> ( ( ( G ` k ) supp Z ) = (/) <-> ( G ` k ) = ( B X. { Z } ) ) )
78 74 75 76 77 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( ( ( G ` k ) supp Z ) = (/) <-> ( G ` k ) = ( B X. { Z } ) ) )
79 78 biimpar 
 |-  ( ( ( ph /\ k e. A ) /\ ( G ` k ) = ( B X. { Z } ) ) -> ( ( G ` k ) supp Z ) = (/) )
80 65 67 68 79 syl21anc 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( ( G ` k ) supp Z ) = (/) )
81 80 ralrimiva 
 |-  ( ph -> A. k e. ( A \ ( G supp ( B X. { Z } ) ) ) ( ( G ` k ) supp Z ) = (/) )
82 nfcv 
 |-  F/_ k ( A \ ( G supp ( B X. { Z } ) ) )
83 82 iunxdif3 
 |-  ( A. k e. ( A \ ( G supp ( B X. { Z } ) ) ) ( ( G ` k ) supp Z ) = (/) -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z ) )
84 81 83 syl 
 |-  ( ph -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z ) )
85 dfin4 
 |-  ( A i^i ( G supp ( B X. { Z } ) ) ) = ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) )
86 suppssdm 
 |-  ( G supp ( B X. { Z } ) ) C_ dom G
87 86 23 fssdm 
 |-  ( ph -> ( G supp ( B X. { Z } ) ) C_ A )
88 sseqin2 
 |-  ( ( G supp ( B X. { Z } ) ) C_ A <-> ( A i^i ( G supp ( B X. { Z } ) ) ) = ( G supp ( B X. { Z } ) ) )
89 87 88 sylib 
 |-  ( ph -> ( A i^i ( G supp ( B X. { Z } ) ) ) = ( G supp ( B X. { Z } ) ) )
90 85 89 eqtr3id 
 |-  ( ph -> ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) = ( G supp ( B X. { Z } ) ) )
91 90 iuneq1d 
 |-  ( ph -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
92 84 91 eqtr3d 
 |-  ( ph -> U_ k e. A ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
93 92 adantr 
 |-  ( ( ph /\ x e. A ) -> U_ k e. A ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
94 64 93 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
95 5 adantr 
 |-  ( ( ph /\ x e. A ) -> Z e. D )
96 58 94 21 95 suppssr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) -> ( ( G ` x ) ` y ) = Z )
97 96 adantr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = Z )
98 56 97 eqtr3d 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> C = Z )
99 48 55 98 3eqtrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
100 99 adantl3r 
 |-  ( ( ( ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
101 elxp2 
 |-  ( z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) <-> E. x e. A E. y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) z = <. x , y >. )
102 101 bilani 
 |-  ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> E. x e. A E. y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) z = <. x , y >. )
103 100 102 r19.29vva 
 |-  ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
104 103 adantlr 
 |-  ( ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
105 simpr 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) )
106 difxp 
 |-  ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) = ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) )
107 105 106 eleqtrdi 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> z e. ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
108 elun 
 |-  ( z e. ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) <-> ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) \/ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
109 107 108 sylib 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) \/ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
110 46 104 109 mpjaodan 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
111 9 110 suppss 
 |-  ( ph -> ( F supp Z ) C_ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )